diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index 2fc755fd4f42..0d953a914df3 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -113,12 +113,12 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
     | Expr.letE n type val body _ =>
       withLetDecl n (← loop below type) (← loop below val) fun x => do
         mkLetFVars #[x] (← loop below (body.instantiate1 x)) (usedLetOnly := false)
-    | Expr.mdata d b     =>
-      if let some _ := getRecAppSyntax? e then
-        loop below b
+    | Expr.mdata d b =>
+      if let some stx := getRecAppSyntax? e then
+        withRef stx <| loop below b
       else
         return mkMData d (← loop below b)
-    | Expr.proj n i e    => return mkProj n i (← loop below e)
+    | Expr.proj n i e => return mkProj n i (← loop below e)
     | Expr.app _ _ =>
       let processApp (e : Expr) : StateRefT (HasConstCache recFnName) M Expr :=
         e.withApp fun f args => do
diff --git a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
index 5264fad15b89..b865b4614d16 100644
--- a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
@@ -23,7 +23,11 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
     | Expr.letE n type val body _ =>
       withLetDecl n (← loop type) (← loop val) fun x => do
         mkLetFVars #[x] (← loop (body.instantiate1 x))
-    | Expr.mdata d e     => return mkMData d (← loop e)
+    | Expr.mdata d b => do
+      if let some stx := getRecAppSyntax? e then
+        withRef stx <| loop b
+      else
+        return mkMData d (← loop b)
     | Expr.proj n i e    => return mkProj n i (← loop e)
     | Expr.app _ _ =>
       let processApp (e : Expr) : M Expr := do
diff --git a/tests/lean/terminationFailure.lean.expected.out b/tests/lean/terminationFailure.lean.expected.out
index 0319f93eaf19..2966b4cc4dc2 100644
--- a/tests/lean/terminationFailure.lean.expected.out
+++ b/tests/lean/terminationFailure.lean.expected.out
@@ -9,7 +9,7 @@ f (x : Nat) : Nat
 f.g (a✝ : Nat) : Nat
 1
 2
-terminationFailure.lean:20:4-20:5: error: fail to show termination for
+terminationFailure.lean:24:9-24:12: error: fail to show termination for
   h
 with errors
 argument #1 was not used for structural recursion
diff --git a/tests/lean/wf1.lean.expected.out b/tests/lean/wf1.lean.expected.out
index aa8c1839cdad..761deed9fbde 100644
--- a/tests/lean/wf1.lean.expected.out
+++ b/tests/lean/wf1.lean.expected.out
@@ -1,4 +1,4 @@
-wf1.lean:1:4-1:5: error: fail to show termination for
+wf1.lean:3:12-3:19: error: fail to show termination for
   g
 with errors
 argument #1 was not used for structural recursion