diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index e2b1942338..58ecd81b62 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -111,7 +111,7 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
     preDefWith.termination.terminationBy? matches some {structural := true, ..}
   for preDef in preDefs do
     if let .some termBy := preDef.termination.terminationBy? then
-      if !preDefsWithout.isEmpty then
+      if !structural && !preDefsWithout.isEmpty then
         let m := MessageData.andList (preDefsWithout.toList.map (m!"{·.declName}"))
         let doOrDoes := if preDefsWithout.size = 1 then "does" else "do"
         logErrorAt termBy.ref (m!"Incomplete set of `termination_by` annotations:\n"++
@@ -135,13 +135,12 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
 /--
 Elaborates the `TerminationHint` in the clique to `TerminationArguments`
 -/
-def elabTerminationByHints (preDefs : Array PreDefinition) : TermElabM (Option TerminationArguments) := do
-  let tas ← preDefs.mapM fun preDef => do
+def elabTerminationByHints (preDefs : Array PreDefinition) : TermElabM (Array (Option TerminationArgument)) := do
+  preDefs.mapM fun preDef => do
     let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
     let hints := preDef.termination
     hints.terminationBy?.mapM
       (TerminationArgument.elab preDef.declName preDef.type arity hints.extraParams ·)
-  return tas.sequenceMap id -- only return something if every function has a hint
 
 def shouldUseStructural (preDefs : Array PreDefinition) : Bool :=
   preDefs.any fun preDef =>
@@ -188,16 +187,16 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       try
         checkCodomainsLevel preDefs
         checkTerminationByHints preDefs
-        let termArgs ← elabTerminationByHints preDefs
+        let termArg?s ← elabTerminationByHints preDefs
         if shouldUseStructural preDefs then
-          structuralRecursion preDefs termArgs
+          structuralRecursion preDefs termArg?s
         else if shouldUseWF preDefs then
-          wfRecursion preDefs termArgs
+          wfRecursion preDefs termArg?s
         else
           withRef (preDefs[0]!.ref) <| mapError
             (orelseMergeErrors
-              (structuralRecursion preDefs termArgs)
-              (wfRecursion preDefs termArgs))
+              (structuralRecursion preDefs termArg?s)
+              (wfRecursion preDefs termArg?s))
             (fun msg =>
               let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
               m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
index d9267e226d..99e1660541 100644
--- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
@@ -4,12 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
+import Lean.Elab.PreDefinition.TerminationArgument
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.RecArgInfo
 
 namespace Lean.Elab.Structural
 open Meta
 
+def prettyParam (xs : Array Expr) (i : Nat) : MetaM MessageData := do
+  let x := xs[i]!
+  let n ← x.fvarId!.getUserName
+  addMessageContextFull <| if n.hasMacroScopes then m!"#{i+1}" else m!"{x}"
+
+def prettyRecArg (xs : Array Expr) (value : Expr) (recArgInfo : RecArgInfo) : MetaM MessageData := do
+  lambdaTelescope value fun ys _ => prettyParam (xs ++ ys) recArgInfo.recArgPos
+
+def prettyParameterSet (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
+    (recArgInfos : Array RecArgInfo) : MetaM MessageData := do
+  if fnNames.size = 1 then
+    return m!"parameter " ++ (← prettyRecArg xs values[0]! recArgInfos[0]!)
+  else
+    let mut l := #[]
+    for fnName in fnNames, value in values, recArgInfo in recArgInfos do
+      l := l.push m!"{(← prettyRecArg xs value recArgInfo)} of {fnName}"
+    return m!"parameters " ++ .andList l.toList
+
 private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := Id.run do
   let mut minPos := xs.size
   for index in indices do
@@ -92,47 +111,139 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
       throwError "the index #{i+1} exceeds {xs.size}, the number of parameters"
 
 /--
-  Runs `k` on all argument indices, until it succeeds.
-  We use this argument to justify termination using the auxiliary `brecOn` construction.
+Collects the `RecArgInfos` for one function, and returns a report for why the others were not
+considered.
 
-  We give preference for arguments that are *not* indices of inductive types of other arguments.
-  See issue #837 for an example where we can show termination using the index of an inductive family, but
-  we don't get the desired definitional equalities.
+The `xs` are the fixed parameters, `value` the body with the fixed prefix instantiated.
 
-  `value` is the function value (including fixed parameters)
+Takes the optional user annotations into account (`termArg?`). If this is given and the argument
+is unsuitable, throw an error.
 -/
-partial def tryAllArgs (value : Expr) (k : Nat → M α) : M α := do
-  -- It's improtant to keep the call to `k` outside the scope of `lambdaTelescope`:
-  -- The tactics in the IndPred construction search the full local context, so we must not have
-  -- extra FVars there
-  let (indices, nonIndices) ← lambdaTelescope value fun xs _ => do
-    let indicesRef : IO.Ref (Array Nat) ← IO.mkRef {}
-    for x in xs do
-      let xType ← inferType x
-      /- Traverse all sub-expressions in the type of `x` -/
-      forEachExpr xType fun e =>
-        /- If `e` is an inductive family, we store in `indicesRef` all variables in `xs` that occur in "index positions". -/
-        matchConstInduct e.getAppFn (fun _ => pure ()) fun info _ => do
-          if info.numIndices > 0 && info.numParams + info.numIndices == e.getAppNumArgs then
-            for arg in e.getAppArgs[info.numParams:] do
-              forEachExpr arg fun e => do
-                if let .some idx := xs.getIdx? e then
-                  indicesRef.modify (·.push idx)
-    let indices ← indicesRef.get
-    let nonIndices := (Array.range xs.size).filter (fun i => !(indices.contains i))
-    return (indices, nonIndices)
+def getRecArgInfos (fnName : Name) (xs : Array Expr) (value : Expr)
+    (termArg? : Option TerminationArgument) : MetaM (Array RecArgInfo × MessageData) := do
+  lambdaTelescope value fun ys _ => do
+    if let .some termArg := termArg? then
+      -- User explictly asked to use a certain argument, so throw errors eagerly
+      let recArgInfo ← withRef termArg.ref do
+        mapError (f := (m!"cannot use specified parameter for structural recursion:{indentD ·}")) do
+          getRecArgInfo fnName xs.size (xs ++ ys) (← termArg.structuralArg)
+      return (#[recArgInfo], m!"")
+    else
+      let mut recArgInfos := #[]
+      let mut report : MessageData := m!""
+      -- No `termination_by`, so try all, and remember the errors
+      for idx in [:xs.size + ys.size] do
+        try
+          let recArgInfo ← getRecArgInfo fnName xs.size (xs ++ ys) idx
+          recArgInfos := recArgInfos.push recArgInfo
+        catch e =>
+          report := report ++ (m!"Not considering parameter {← prettyParam (xs ++ ys) idx} of {fnName}:" ++
+            indentD e.toMessageData) ++ "\n"
+      trace[Elab.definition.structural] "getRecArgInfos report: {report}"
+      return (recArgInfos, report)
 
-  let mut errors : Array MessageData := Array.mkArray (indices.size  + nonIndices.size) m!""
-  let saveState ← get -- backtrack the state for each argument
-  for i in id (nonIndices ++ indices) do
-    trace[Elab.definition.structural] "findRecArg i: {i}"
-    try
-      set saveState
-      return (← k i)
-    catch e => errors := errors.set! i e.toMessageData
-  throwError
-    errors.foldl
-      (init := m!"structural recursion cannot be used:")
-      (f := (· ++ Format.line ++ Format.line ++ .))
+
+/--
+Reorders the `RecArgInfos` of one function to put arguments that are indices of other arguments
+last.
+See issue #837 for an example where we can show termination using the index of an inductive family, but
+we don't get the desired definitional equalities.
+-/
+def nonIndicesFirst (recArgInfos : Array RecArgInfo) : Array RecArgInfo := Id.run do
+  let mut indicesPos : HashSet Nat := {}
+  for recArgInfo in recArgInfos do
+    for pos in recArgInfo.indicesPos do
+      indicesPos := indicesPos.insert pos
+  let (indices,nonIndices) := recArgInfos.partition (indicesPos.contains ·.recArgPos)
+  return nonIndices ++ indices
+
+private def dedup [Monad m] (eq : α → α → m Bool) (xs : Array α) : m (Array α) := do
+  let mut ret := #[]
+  for x in xs do
+    unless (← ret.anyM (eq · x)) do
+      ret := ret.push x
+  return ret
+
+/--
+Given the `RecArgInfo`s of all the recursive functions, find the inductive groups to consider.
+-/
+def inductiveGroups (recArgInfos : Array RecArgInfo) : MetaM (Array IndGroupInst) :=
+  dedup IndGroupInst.isDefEq (recArgInfos.map (·.indGroupInst))
+
+/--
+Filters the `recArgInfos` by those that describe an argument that's part of the recursive inductive
+group `group`.
+
+
+Anticipating support for nested inductives this function has the ability to change the `recArgInfo`.
+Consider
+```
+inductive Tree where | node : List Tree → Tree
+```
+then when we look for arguments whose type is part of the group `Tree`, we want to also consider
+the argument of type `List Tree`, even though that argument’s `RecArgInfo` refers to initially to
+`List`.
+-/
+def argsInGroup (group : IndGroupInst) (_xs : Array Expr) (_value : Expr)
+    (recArgInfos : Array RecArgInfo) : MetaM (Array RecArgInfo) := do
+  recArgInfos.filterM (group.isDefEq ·.indGroupInst)
+
+def maxCombinationSize : Nat := 10
+
+def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
+  if xss.foldl (· * ·.size) 1 > maxCombinationSize then
+    none
+  else
+    let rec go i acc : Array (Array α):=
+      if h : i < xss.size then
+        xss[i].concatMap fun x => go (i + 1) (acc.push x)
+      else
+        #[acc]
+    some (go 0 #[])
+
+
+def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
+   (termArg?s : Array (Option TerminationArgument)) (k : Array RecArgInfo → M α) : M α := do
+  let mut report := m!""
+  -- Gather information on all possible recursive arguments
+  let mut recArgInfoss := #[]
+  for fnName in fnNames, value in values, termArg? in termArg?s do
+    let (recArgInfos, thisReport) ← getRecArgInfos fnName xs value termArg?
+    report := report ++ thisReport
+    recArgInfoss := recArgInfoss.push recArgInfos
+  -- Put non-indices first
+  recArgInfoss := recArgInfoss.map nonIndicesFirst
+  trace[Elab.definition.structural] "recArgInfoss: {recArgInfoss.map (·.map (·.recArgPos))}"
+  -- Inductive groups to consider
+  let groups ← inductiveGroups recArgInfoss.flatten
+  trace[Elab.definition.structural] "inductive groups: {groups}"
+  if groups.isEmpty then
+    report := report ++ "no parameters suitable for structural recursion"
+  -- Consider each group
+  for group in groups do
+    -- Select those RecArgInfos that are compatible with this inductive group
+    let mut recArgInfoss' := #[]
+    for value in values, recArgInfos in recArgInfoss do
+      recArgInfoss' := recArgInfoss'.push (← argsInGroup group xs value recArgInfos)
+    if let some idx := recArgInfoss'.findIdx? (·.isEmpty) then
+      report := report ++ m!"Skipping arguments of type {group}, as {fnNames[idx]!} has no compatible argument.\n"
+      continue
+    if let some combs := allCombinations recArgInfoss' then
+      for comb in combs do
+        try
+          -- TODO: Here we used to save and restore the state. But should the `try`-`catch`
+          -- not suffice?
+          let r ← k comb
+          trace[Elab.definition.structural] "tryTellArgs report:\n{report}"
+          return r
+        catch e =>
+          let m ← prettyParameterSet fnNames xs values comb
+          report := report ++ m!"Cannot use {m}:{indentD e.toMessageData}\n"
+    else
+          report := report ++ m!"Too many possible combinations of parameters of type {group} (or " ++
+            m!"please indicate the recursive argument explicitly using `termination_by structural`).\n"
+  report := m!"failed to infer structural recursion:\n" ++ report
+  trace[Elab.definition.structural] "tryTellArgs:\n{report}"
+  throwError report
 
 end Lean.Elab.Structural
diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean
index 0b59d025e0..d98abdce6c 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean
@@ -89,98 +89,68 @@ def getMutualFixedPrefix (preDefs : Array PreDefinition) : M Nat :=
           return true
     resultRef.get
 
-/-- Checks that all parameter types are mutually inductive -/
-private def checkAllFromSameClique (recArgInfos : Array RecArgInfo) : MetaM Unit := do
-  for recArgInfo in recArgInfos do
-    unless recArgInfos[0]!.indGroupInst.all.contains recArgInfo.indName! do
-      throwError m!"Cannot use structural mutual recursion: The recursive argument of " ++
-        m!"{recArgInfos[0]!.fnName} is of type {recArgInfos[0]!.indName!}, " ++
-        m!"the recursive argument of {recArgInfo.fnName} is of type " ++
-            m!"{recArgInfo.indName!}, and these are not mutually recursive."
+private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr)
+    (recArgInfos : Array RecArgInfo) : M (Array PreDefinition) := do
+  let values ← preDefs.mapM (instantiateLambda ·.value xs)
+  let indInfo ← getConstInfoInduct recArgInfos[0]!.indName!
+  if ← isInductivePredicate indInfo.name then
+    -- Here we branch off to the IndPred construction, but only for non-mutual functions
+    unless preDefs.size = 1 do
+      throwError "structural mutual recursion over inductive predicates is not supported"
+    trace[Elab.definition.structural] "Using mkIndPred construction"
+    let preDef := preDefs[0]!
+    let recArgInfo := recArgInfos[0]!
+    let value := values[0]!
+    let valueNew ← mkIndPredBRecOn recArgInfo value
+    let valueNew ← mkLambdaFVars xs valueNew
+    trace[Elab.definition.structural] "Nonrecursive value:{indentExpr valueNew}"
+    check valueNew
+    return #[{ preDef with value := valueNew }]
 
-private def elimMutualRecursion (preDefs : Array PreDefinition) (recArgPoss : Array Nat) : M (Array PreDefinition) := do
+  -- Sort the (indices of the) definitions by their position in indInfo.all
+  let positions : Positions := .groupAndSort (·.indName!) recArgInfos indInfo.all.toArray
+
+  -- Construct the common `.brecOn` arguments
+  let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
+  let brecOnConst ← mkBRecOnConst recArgInfos positions motives
+  let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
+  let FArgs ← (recArgInfos.zip  (values.zip FTypes)).mapM fun (r, (v, t)) =>
+    mkBRecOnF recArgInfos positions r v t
+  -- Assemble the individual `.brecOn` applications
+  let valuesNew ← (Array.zip recArgInfos values).mapIdxM fun i (r, v) =>
+    mkBrecOnApp positions i brecOnConst FArgs r v
+  -- Abstract over the fixed prefixed
+  let valuesNew ← valuesNew.mapM (mkLambdaFVars xs ·)
+  return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
+
+private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) :
+    M (Array Nat × Array PreDefinition) := do
   withoutModifyingEnv do
     preDefs.forM (addAsAxiom ·)
-    let names := preDefs.map (·.declName)
+    let fnNames := preDefs.map (·.declName)
     let preDefs ← preDefs.mapM fun preDef =>
-      return { preDef with value := (← preprocess preDef.value names) }
+      return { preDef with value := (← preprocess preDef.value fnNames) }
 
     -- The syntactically fixed arguments
     let maxNumFixed ← getMutualFixedPrefix preDefs
 
-    -- We do two passes to get the RecArgInfo values.
-    -- From the first pass, we only keep the mininum of the `numFixed` reported.
-    let numFixed ← lambdaBoundedTelescope preDefs[0]!.value maxNumFixed fun xs _ => do
+    lambdaBoundedTelescope preDefs[0]!.value maxNumFixed fun xs _ => do
       assert! xs.size = maxNumFixed
       let values ← preDefs.mapM (instantiateLambda ·.value xs)
 
-      let recArgInfos ← preDefs.mapIdxM fun i preDef => do
-        let recArgPos := recArgPoss[i]!
-        let value := values[i]!
-        lambdaTelescope value fun ys _value => do
-          getRecArgInfo preDef.declName maxNumFixed (xs ++ ys) recArgPos
-
-      checkAllFromSameClique recArgInfos
-
-      -- Check that the inductive parameters agree. This also ensures that they only depend on the
-      -- trimmed prefix (minimum of all `.numFixed`).
-      for recArgInfo in recArgInfos[1:] do
-        let ok ← IndGroupInst.isDefEq recArgInfo.indGroupInst recArgInfos[0]!.indGroupInst
-        unless ok do
-          throwError m!"The inductive type of the recursive parameter of {recArgInfos[0]!.fnName} " ++
-            m!"and {recArgInfo.fnName} have different parameters:" ++
-            indentD m!"{recArgInfos[0]!.indGroupInst.params}" ++
-            indentD m!"{recArgInfo.indGroupInst.params}"
-
-      return (recArgInfos.map (·.numFixed)).foldl Nat.min maxNumFixed
-
-    if numFixed < maxNumFixed then
-      trace[Elab.definition.structural] "Reduced numFixed from {maxNumFixed} to {numFixed}"
-
-    -- Now we bring exactly that `numFixed` parameter into scope.
-    lambdaBoundedTelescope preDefs[0]!.value numFixed fun xs _ => do
-      assert! xs.size = numFixed
-      let values ← preDefs.mapM (instantiateLambda ·.value xs)
-
-      let recArgInfos ← preDefs.mapIdxM fun i preDef => do
-        let recArgPos := recArgPoss[i]!
-        let value := values[i]!
-        lambdaTelescope value fun ys _value => do
-          getRecArgInfo preDef.declName numFixed (xs ++ ys) recArgPos
-
-      -- Two passes should suffice
-      assert! recArgInfos.all (·.numFixed = numFixed)
-
-      let indInfo ← getConstInfoInduct recArgInfos[0]!.indName!
-      if ← isInductivePredicate indInfo.name then
-        -- Here we branch off to the IndPred construction, but only for non-mutual functions
-        unless preDefs.size = 1 do
-          throwError "structural mutual recursion over inductive predicates is not supported"
-        trace[Elab.definition.structural] "Using mkIndPred construction"
-        let preDef := preDefs[0]!
-        let recArgInfo := recArgInfos[0]!
-        let value := values[0]!
-        let valueNew ← mkIndPredBRecOn recArgInfo value
-        let valueNew ← mkLambdaFVars xs valueNew
-        trace[Elab.definition.structural] "Nonrecursive value:{indentExpr valueNew}"
-        check valueNew
-        return #[{ preDef with value := valueNew }]
-
-      -- Sort the (indices of the) definitions by their position in indInfo.all
-      let positions : Positions := .groupAndSort (·.indName!) recArgInfos indInfo.all.toArray
-
-      -- Construct the common `.brecOn` arguments
-      let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
-      let brecOnConst ← mkBRecOnConst recArgInfos positions motives
-      let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
-      let FArgs ← (recArgInfos.zip  (values.zip FTypes)).mapM fun (r, (v, t)) =>
-        mkBRecOnF recArgInfos positions r v t
-      -- Assemble the individual `.brecOn` applications
-      let valuesNew ← (Array.zip recArgInfos values).mapIdxM fun i (r, v) =>
-        mkBrecOnApp positions i brecOnConst FArgs r v
-      -- Abstract over the fixed prefixed
-      let valuesNew ← valuesNew.mapM (mkLambdaFVars xs ·)
-      return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
+      tryAllArgs fnNames xs values termArg?s fun recArgInfos => do
+        let recArgPoss := recArgInfos.map (·.recArgPos)
+        trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
+        let numFixed := recArgInfos.foldl (·.min ·.numFixed) maxNumFixed
+        if numFixed < maxNumFixed then
+          trace[Elab.definition.structural] "Reduced numFixed from {maxNumFixed} to {numFixed}"
+        -- We may have decreased the number of arguments we consider fixed, so update
+        -- the recArgInfos, remove the extra arguments from local environment, and recalculate value
+        let recArgInfos := recArgInfos.map ({· with numFixed := numFixed })
+        withErasedFVars (xs.extract numFixed xs.size |>.map (·.fvarId!)) do
+          let xs := xs[:numFixed]
+          let preDefs' ← elimMutualRecursion preDefs xs recArgInfos
+          return (recArgPoss, preDefs')
 
 def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
   if let some ref := preDef.termination.terminationBy?? then
@@ -190,34 +160,20 @@ def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
     let stx ← termArg.delab arity (extraParams := preDef.termination.extraParams)
     Tactic.TryThis.addSuggestion ref stx
 
-private def inferRecArgPos (preDefs : Array PreDefinition)
-    (termArgs? : Option TerminationArguments) : M (Array Nat × Array PreDefinition) := do
-  withoutModifyingEnv do
-    if let some termArgs := termArgs? then
-      let recArgPoss ← termArgs.mapM (·.structuralArg)
-      let preDefsNew ← elimMutualRecursion preDefs recArgPoss
-      return (recArgPoss, preDefsNew)
-    else
-      let #[preDef] := preDefs
-        | throwError "mutual structural recursion requires explicit `termination_by` clauses"
-      -- Use termination_by annotation to find argument to recurse on, or just try all
-      tryAllArgs preDef.value fun i =>
-        mapError (f := fun msg => m!"argument #{i+1} cannot be used for structural recursion{indentD msg}") do
-          let preDefsNew ← elimMutualRecursion #[preDef] #[i]
-          return (#[i], preDefsNew)
 
-def structuralRecursion (preDefs : Array PreDefinition) (termArgs? : Option TerminationArguments) : TermElabM Unit := do
-  let ((recArgPoss, preDefsNonRec), state) ← run <| inferRecArgPos preDefs termArgs?
+def structuralRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
+  let names := preDefs.map (·.declName)
+  let ((recArgPoss, preDefsNonRec), state) ← run <| inferRecArgPos preDefs termArg?s
   for recArgPos in recArgPoss, preDef in preDefs do
     reportTermArg preDef recArgPos
   state.addMatchers.forM liftM
   preDefsNonRec.forM fun preDefNonRec => do
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
     -- state.addMatchers.forM liftM
-    mapError (addNonRec preDefNonRec (applyAttrAfterCompilation := false)) fun msg =>
-      m!"structural recursion failed, produced type incorrect term{indentD msg}"
-    -- We create the `_unsafe_rec` before we abstract nested proofs.
-    -- Reason: the nested proofs may be referring to the _unsafe_rec.
+    mapError (f := (m!"structural recursion failed, produced type incorrect term{indentD ·}")) do
+      -- We create the `_unsafe_rec` before we abstract nested proofs.
+      -- Reason: the nested proofs may be referring to the _unsafe_rec.
+      addNonRec preDefNonRec (applyAttrAfterCompilation := false) (all := names.toList)
   let preDefs ← preDefs.mapM (eraseRecAppSyntax ·)
   addAndCompilePartialRec preDefs
   for preDef in preDefs, recArgPos in recArgPoss do
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index 35ff51f632..bbe5b191da 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -86,7 +86,8 @@ def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Ar
     let xs : Array Expr := xs[fixedPrefixSize:]
     xs.mapM (·.fvarId!.getUserName)
 
-def wfRecursion (preDefs : Array PreDefinition) (termArgs? : Option TerminationArguments) : TermElabM Unit := do
+def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
+  let termArgs? := termArg?s.sequenceMap id -- Either all or none, checked by `elabTerminationByHints`
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← preprocess preDef.value) }
   let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do
diff --git a/tests/lean/1673.lean.expected.out b/tests/lean/1673.lean.expected.out
index 1fdb96a40c..972889b428 100644
--- a/tests/lean/1673.lean.expected.out
+++ b/tests/lean/1673.lean.expected.out
@@ -1,12 +1,11 @@
 1673.lean:1:4-1:9: error: fail to show termination for
   foo.a
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Not considering parameter n of foo.a:
   it is unchanged in the recursive calls
-
-argument #2 cannot be used for structural recursion
+Not considering parameter nope of foo.a:
   it is unchanged in the recursive calls
+no parameters suitable for structural recursion
 
 well-founded recursion cannot be used, 'foo.a' does not take any (non-fixed) arguments
diff --git a/tests/lean/guessLex.lean b/tests/lean/guessLex.lean
index 9a8c6418e6..0f92fe4246 100644
--- a/tests/lean/guessLex.lean
+++ b/tests/lean/guessLex.lean
@@ -35,6 +35,7 @@ mutual
 def even : Nat → Bool
   | 0 => true
   | .succ n => not (odd n)
+decreasing_by decreasing_tactic
 def odd : Nat → Bool
   | 0 => false
   | .succ n => not (even n)
@@ -44,6 +45,7 @@ mutual
 def evenWithFixed (m : String) : Nat → Bool
   | 0 => true
   | .succ n => not (oddWithFixed m n)
+decreasing_by decreasing_tactic
 def oddWithFixed (m : String) : Nat → Bool
   | 0 => false
   | .succ n => not (evenWithFixed m n)
@@ -81,6 +83,7 @@ def blowup : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat
 def confuseLex1 : Nat → @PSigma Nat (fun _ => Nat) → Nat
   | 0, _p => 0
   | .succ n, ⟨x,y⟩ => confuseLex1 n ⟨x, .succ y⟩
+decreasing_by decreasing_tactic
 
 def confuseLex2 : @PSigma Nat (fun _ => Nat) → Nat
   | ⟨_,0⟩ => 0
diff --git a/tests/lean/guessLex.lean.expected.out b/tests/lean/guessLex.lean.expected.out
index 3cedc21391..f584037118 100644
--- a/tests/lean/guessLex.lean.expected.out
+++ b/tests/lean/guessLex.lean.expected.out
@@ -23,6 +23,8 @@ termination_by (m, n)
 Inferred termination argument:
 termination_by x1 x2 x3 x4 x5 x6 x7 x8 => (x8, x7, x6, x5, x4, x3, x2, x1)
 Inferred termination argument:
+termination_by x1 => x1
+Inferred termination argument:
 termination_by x1 => sizeOf x1
 Inferred termination argument:
 termination_by n m => (n, sizeOf m)
diff --git a/tests/lean/guessLexDiff.lean.expected.out b/tests/lean/guessLexDiff.lean.expected.out
index 1f7bff5c9e..7abee8bc37 100644
--- a/tests/lean/guessLexDiff.lean.expected.out
+++ b/tests/lean/guessLexDiff.lean.expected.out
@@ -13,15 +13,14 @@ termination_by (xs.size - i, i)
 guessLexDiff.lean:84:4-84:11: error: fail to show termination for
   failure
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Not considering parameter xs of failure:
   it is unchanged in the recursive calls
-
-argument #2 cannot be used for structural recursion
+Cannot use parameter i:
   failed to eliminate recursive application
     _root_.failure xs i
 
+
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
@@ -44,7 +43,15 @@ guessLexDiff.lean:102:4-102:18: error: fail to show termination for
   mutual_failure
   mutual_failure2
 with errors
-mutual structural recursion requires explicit `termination_by` clauses
+failed to infer structural recursion:
+Not considering parameter xs of mutual_failure:
+  it is unchanged in the recursive calls
+Not considering parameter xs of mutual_failure2:
+  it is unchanged in the recursive calls
+Cannot use parameters i of mutual_failure and i of mutual_failure2:
+  failed to eliminate recursive application
+    mutual_failure2 xs i
+
 
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out
index 7cced5e609..f1e02e1e1c 100644
--- a/tests/lean/guessLexFailures.lean.expected.out
+++ b/tests/lean/guessLexFailures.lean.expected.out
@@ -1,15 +1,14 @@
 guessLexFailures.lean:9:4-9:18: error: fail to show termination for
   nonTerminating
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Cannot use parameter #1:
+  failed to eliminate recursive application
+    nonTerminating n.succ m.succ
+Cannot use parameter #2:
   failed to eliminate recursive application
     nonTerminating n.succ m.succ
 
-argument #2 cannot be used for structural recursion
-  failed to eliminate recursive application
-    nonTerminating n.succ m.succ
 
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
@@ -26,16 +25,17 @@ Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:20:4-20:15: error: fail to show termination for
   noArguments
 with errors
-structural recursion cannot be used:
+failed to infer structural recursion:
+no parameters suitable for structural recursion
 
 well-founded recursion cannot be used, 'noArguments' does not take any (non-fixed) arguments
 guessLexFailures.lean:22:4-22:23: error: fail to show termination for
   noNonFixedArguments
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Not considering parameter n of noNonFixedArguments:
   it is unchanged in the recursive calls
+no parameters suitable for structural recursion
 
 well-founded recursion cannot be used, 'noNonFixedArguments' does not take any (non-fixed) arguments
 guessLexFailures.lean:27:0-33:31: error: Could not find a decreasing measure.
@@ -67,7 +67,17 @@ guessLexFailures.lean:59:6-59:7: error: fail to show termination for
   Mutual.g
   Mutual.h
 with errors
-mutual structural recursion requires explicit `termination_by` clauses
+failed to infer structural recursion:
+Not considering parameter fixed of Mutual.f:
+  it is unchanged in the recursive calls
+Not considering parameter fixed of Mutual.g:
+  it is unchanged in the recursive calls
+Not considering parameter H of Mutual.g:
+  its type True does not have a recursor
+Not considering parameter fixed of Mutual.h:
+  it is unchanged in the recursive calls
+Too many possible combinations of parameters of type Nat (or please indicate the recursive argument explicitly using `termination_by structural`).
+
 
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
@@ -109,15 +119,14 @@ Please use `termination_by` to specify a decreasing measure.
 guessLexFailures.lean:87:4-87:5: error: fail to show termination for
   DuplicatedCall.f
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Cannot use parameter #1:
+  failed to eliminate recursive application
+    DuplicatedCall.f (n + 2) (m + 1)
+Cannot use parameter #2:
   failed to eliminate recursive application
     DuplicatedCall.f (n + 2) (m + 1)
 
-argument #2 cannot be used for structural recursion
-  failed to eliminate recursive application
-    DuplicatedCall.f (n + 2) (m + 1)
 
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
diff --git a/tests/lean/run/issue4671.lean b/tests/lean/run/issue4671.lean
index 264c0d7253..5a06963849 100644
--- a/tests/lean/run/issue4671.lean
+++ b/tests/lean/run/issue4671.lean
@@ -5,13 +5,14 @@ inductive  A (n : Nat) : Type
   | b : A n → A n
 
 /--
-error: its type is an inductive datatype
-  A n
-and the datatype parameter
-  n
-depends on the function parameter
-  n
-which does not come before the varying parameters and before the indices of the recursion parameter.
+error: cannot use specified parameter for structural recursion:
+  its type is an inductive datatype
+    A n
+  and the datatype parameter
+    n
+  depends on the function parameter
+    n
+  which does not come before the varying parameters and before the indices of the recursion parameter.
 -/
 #guard_msgs in
 def A.size (acc n : Nat) : A n → Nat
@@ -27,13 +28,14 @@ inductive Xn (e : Sigma.{0} (· → Type)) (α : Type) : Nat → Type where
 | mk2 {n} (s : e.1) (p : e.2 s → Xn e α n) : Xn e α n
 
 /--
-error: its type is an inductive datatype
-  Xn e (Xn e α n) m
-and the datatype parameter
-  Xn e α n
-depends on the function parameter
-  n
-which does not come before the varying parameters and before the indices of the recursion parameter.
+error: cannot use specified parameter for structural recursion:
+  its type is an inductive datatype
+    Xn e (Xn e α n) m
+  and the datatype parameter
+    Xn e α n
+  depends on the function parameter
+    n
+  which does not come before the varying parameters and before the indices of the recursion parameter.
 -/
 #guard_msgs in
 def Xn.zip {e α m n} : Xn e (Xn e α n) m → Xn e α (n+m+1)
diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean
index 9ce12e9602..8f2f69138a 100644
--- a/tests/lean/run/structuralMutual.lean
+++ b/tests/lean/run/structuralMutual.lean
@@ -1,5 +1,13 @@
 import Lean.Elab.Command
 
+/-!
+Mutual structural recursion.
+
+In this file, we often attach a `termination_by structural` annotation to at least
+one of the functions to force structural recursion. We don't want lean to resort to
+well-founded recursion if structural recursion fails somehow.
+-/
+
 mutual
 inductive A
   | self : A → A
@@ -19,11 +27,11 @@ def A.size : A → Nat
   | .other b => b.size + 1
   | .empty => 0
 termination_by structural x => x
+
 def B.size : B → Nat
   | .self b => b.size + 1
   | .other a => a.size + 1
   | .empty => 0
-termination_by structural x => x
 end
 
 
@@ -87,7 +95,6 @@ def B.subs : (b : B) → (Fin b.size → A ⊕ B)
   | .self b => Fin.lastCases (.inr b) (b.subs)
   | .other a => Fin.lastCases (.inl a) (a.subs)
   | .empty => Fin.elim0
-termination_by structural x => x
 end
 
 
@@ -103,7 +110,6 @@ def B.hasNoBEmpty : B → Prop
   | .self b => b.hasNoBEmpty
   | .other a => a.hasNoBEmpty
   | .empty => False
-termination_by structural x => x
 end
 
 -- Mixing Prop and Nat.
@@ -122,7 +128,6 @@ def B.oddCount : B → Nat
   | .self b => b.oddCount + 1
   | .other a => if a.hasNoAEmpty then 0 else 1
   | .empty => 0
-termination_by structural x => x
 end
 
 -- Higher levels, but the same level `Type u`
@@ -138,7 +143,6 @@ def B.type.{u} : B → Type u
   | .self b => PUnit × b.type
   | .other a => PUnit × a.type
   | .empty => PUnit
-termination_by structural x => x
 end
 
 
@@ -162,7 +166,6 @@ def B.odderCount : B → Nat
   | .self b => b.odderCount + 1
   | .other a => if Nonempty a.strangeType then 0 else 1
   | .empty => 0
-termination_by structural x => x
 end
 
 
@@ -191,7 +194,6 @@ def B.size (m n : Nat): B m n → Nat
   | .self b => b.size + m
   | .other a => a.size + m
   | .empty => 0
-termination_by structural x => x
 end
 
 mutual
@@ -204,7 +206,6 @@ theorem B.size_eq_index (m n : Nat) : (b : B m n) → b.size = n
   | .self b => by dsimp [B.size]; rw [B.size_eq_index]
   | .other a => by dsimp [B.size]; rw [A.size_eq_index]
   | .empty => rfl
-termination_by structural x => x
 end
 
 end Index
@@ -223,7 +224,6 @@ mutual
   def Odd : Nat → Prop
     | 0 => False
     | n+1 => ¬ Even n
-  termination_by structural x => x
 end
 
 mutual
@@ -235,7 +235,6 @@ mutual
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => ! isEven n
-  termination_by structural x => x
 end
 
 theorem isEven_eq_2 (n : Nat) : isEven (n+1) = ! isOdd n := rfl
@@ -301,12 +300,10 @@ def A.weird_size2 : A → Nat
   | .self a => a.weird_size3 + 1
   | .other _ => 0
   | .empty => 0
-termination_by structural x => x
 def A.weird_size3 : A → Nat
   | .self a => a.weird_size1 + 1
   | .other _ => 0
   | .empty => 0
-termination_by structural x => x
 end
 
 -- We have equality
@@ -329,7 +326,10 @@ inductive Tree where
 
 -- Nested recursion does not work (yet)
 
-/-- error: its type NestedWithTuple.Tree is a nested inductive, which is not yet supported -/
+/--
+error: cannot use specified parameter for structural recursion:
+  its type NestedWithTuple.Tree is a nested inductive, which is not yet supported
+-/
 #guard_msgs in
 def Tree.size : Tree → Nat
   | leaf => 0
@@ -348,7 +348,9 @@ inductive A
   | empty
 
 /--
-error: Cannot use structural mutual recursion: The recursive argument of DifferentTypes.A.with_nat is of type DifferentTypes.A, the recursive argument of DifferentTypes.Nat.foo is of type Nat, and these are not mutually recursive.
+error: failed to infer structural recursion:
+Skipping arguments of type A, as DifferentTypes.Nat.foo has no compatible argument.
+Skipping arguments of type Nat, as DifferentTypes.A.with_nat has no compatible argument.
 -/
 #guard_msgs in
 mutual
@@ -359,7 +361,6 @@ termination_by structural x => x
 def Nat.foo : Nat → Nat
   | n+1 => Nat.foo n
   | 0 => A.empty.with_nat
-termination_by structural x => x
 end
 
 end DifferentTypes
@@ -387,7 +388,6 @@ termination_by structural t => t
 def T.size2 (n : Nat) (start : Nat) : T n → Nat
   | .a => 0
   | .b t => 1 + T.size1 n start t
-termination_by structural t => t
 end
 
 end Mutual
@@ -414,7 +414,6 @@ termination_by structural t => t
 
 def B.size (n : Nat) (start : Nat) : B → Nat
   | .a a => 1 + A.size n start (a n)
-termination_by structural t => t
 end
 
 end Mutual2
@@ -430,13 +429,14 @@ inductive  B (n : Nat) : Type
 end
 
 /--
-error: its type is an inductive datatype
-  A n
-and the datatype parameter
-  n
-depends on the function parameter
-  n
-which does not come before the varying parameters and before the indices of the recursion parameter.
+error: cannot use specified parameter for structural recursion:
+  its type is an inductive datatype
+    A n
+  and the datatype parameter
+    n
+  depends on the function parameter
+    n
+  which does not come before the varying parameters and before the indices of the recursion parameter.
 -/
 #guard_msgs in
 set_option linter.constructorNameAsVariable false in
@@ -448,14 +448,14 @@ termination_by structural t => t
 
 def B.size (n : Nat) (m : Nat) : B m → Nat
   | .a a => 1 + A.size m n a
-termination_by structural t => t
 end
 
 end Mutual3
 
 /--
-error: its type FixedIndex.T is an inductive family and indices are not variables
-  T 37
+error: cannot use specified parameter for structural recursion:
+  its type FixedIndex.T is an inductive family and indices are not variables
+    T 37
 -/
 #guard_msgs in
 def T.size2 : T 37 → Nat
@@ -474,13 +474,14 @@ inductive T (n : Nat) : Nat → Type where
   | n : T n n → T n n
 
 /--
-error: its type is an inductive datatype
-  T n n
-and the datatype parameter
-  n
-depends on the function parameter
-  n
-which does not come before the varying parameters and before the indices of the recursion parameter.
+error: cannot use specified parameter for structural recursion:
+  its type is an inductive datatype
+    T n n
+  and the datatype parameter
+    n
+  depends on the function parameter
+    n
+  which does not come before the varying parameters and before the indices of the recursion parameter.
 -/
 #guard_msgs in
 def T.a (n : Nat) : T n n → Nat
@@ -502,9 +503,9 @@ inductive T (n : Nat) : Type where
   | n : T n → T n
 
 /--
-error: The inductive type of the recursive parameter of DifferentParameters.T.a and DifferentParameters.T.b have different parameters:
-  [23]
-  [42]
+error: failed to infer structural recursion:
+Skipping arguments of type T 23, as DifferentParameters.T.b has no compatible argument.
+Skipping arguments of type T 42, as DifferentParameters.T.a has no compatible argument.
 -/
 #guard_msgs in
 mutual
@@ -515,11 +516,79 @@ termination_by structural t => t
 def T.b : T 42 → Nat
   | .z => 0
   | .n t => t.b + 1 + T.a .z
-termination_by structural t => t
 end
 
 end DifferentParameters
 
+namespace ManyCombinations
+-- A datatype with no size function, to avoid well-founded recursion
+
+inductive Nattish
+  | zero
+  | cons : (Nat → Nattish) → Nattish
+
+/--
+error: fail to show termination for
+  ManyCombinations.f
+  ManyCombinations.g
+with errors
+failed to infer structural recursion:
+Too many possible combinations of parameters of type Nattish (or please indicate the recursive argument explicitly using `termination_by structural`).
+
+
+Could not find a decreasing measure.
+The arguments relate at each recursive call as follows:
+(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
+Call from ManyCombinations.f to ManyCombinations.g at 571:15-29:
+   #1 #2 #3 #4
+#5  ?  ?  ?  ?
+#6  ?  =  ?  ?
+#7  ?  ?  =  ?
+#8  ?  ?  ?  =
+Call from ManyCombinations.g to ManyCombinations.f at 574:15-29:
+   #5 #6 #7 #8
+#1  _  _  _  _
+#2  _  =  _  _
+#3  _  _  =  _
+#4  _  _  _  =
+
+
+#1: sizeOf a
+#2: sizeOf b
+#3: sizeOf c
+#4: sizeOf d
+#5: sizeOf a
+#6: sizeOf b
+#7: sizeOf c
+#8: sizeOf d
+
+Please use `termination_by` to specify a decreasing measure.
+-/
+#guard_msgs in
+mutual
+def f (a b c d : Nattish) : Nat := match a with
+  | .zero => 0
+  | .cons n => g (n 23) b c d
+def g (a b c d : Nattish) : Nat := match a with
+  | .zero => 0
+  | .cons n => f (n 42) b c d
+end
+
+-- specifying one `termination_by structural` helps
+
+#guard_msgs in
+mutual
+def f' (a b c d : Nattish) : Nat := match a with
+  | .zero => 0
+  | .cons n => g' (n 23) b c d
+termination_by structural a
+def g' (a b c d : Nattish) : Nat := match a with
+  | .zero => 0
+  | .cons n => f' (n 42) b c d
+end
+
+end ManyCombinations
+
 namespace FunIndTests
 
 -- FunInd does not handle mutual structural recursion yet, so make sure we error
diff --git a/tests/lean/run/terminationByStructurally.lean b/tests/lean/run/terminationByStructurally.lean
index ec9567da48..2137a7b5de 100644
--- a/tests/lean/run/terminationByStructurally.lean
+++ b/tests/lean/run/terminationByStructurally.lean
@@ -18,14 +18,18 @@ termination_by «structural»
 namespace Errors
 -- A few error conditions
 
-/-- error: it is unchanged in the recursive calls -/
+/--
+error: cannot use specified parameter for structural recursion:
+  it is unchanged in the recursive calls
+-/
 #guard_msgs in
 def foo1 (n : Nat) : Nat := foo1 n
 termination_by structural n
 
 /--
-error: its type Nat.le is an inductive family and indices are not variables
-  n.succ.le 100
+error: cannot use specified parameter for structural recursion:
+  its type Nat.le is an inductive family and indices are not variables
+    n.succ.le 100
 -/
 #guard_msgs in
 def foo2 (n : Nat) (h : n < 100) : Nat := match n with
@@ -43,8 +47,10 @@ def foo3 (n : Nat) : Nat → Nat := match n with
 termination_by structural m => m
 
 /--
-error: failed to eliminate recursive application
-  ackermann (n + 1) m
+error: failed to infer structural recursion:
+Cannot use parameter n:
+  failed to eliminate recursive application
+    ackermann (n + 1) m
 -/
 #guard_msgs in
 def ackermann (n m : Nat) := match n, m with
@@ -54,8 +60,10 @@ def ackermann (n m : Nat) := match n, m with
 termination_by structural n
 
 /--
-error: failed to eliminate recursive application
-  ackermann2 n 1
+error: failed to infer structural recursion:
+Cannot use parameter m:
+  failed to eliminate recursive application
+    ackermann2 n 1
 -/
 #guard_msgs in
 def ackermann2 (n m : Nat) := match n, m with
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
index 314a8da072..3958cd21a7 100644
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -1,7 +1,8 @@
 sanitychecks.lean:1:8-1:15: error: fail to show termination for
   unsound
 with errors
-structural recursion cannot be used:
+failed to infer structural recursion:
+no parameters suitable for structural recursion
 
 well-founded recursion cannot be used, 'unsound' does not take any (non-fixed) arguments
 sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
diff --git a/tests/lean/terminationFailure.lean.expected.out b/tests/lean/terminationFailure.lean.expected.out
index 9f4d65431f..cc8cf78575 100644
--- a/tests/lean/terminationFailure.lean.expected.out
+++ b/tests/lean/terminationFailure.lean.expected.out
@@ -2,7 +2,11 @@ terminationFailure.lean:7:2-7:3: error: fail to show termination for
   f.g
   f
 with errors
-mutual structural recursion requires explicit `termination_by` clauses
+failed to infer structural recursion:
+Cannot use parameters #1 of f.g and x of f:
+  failed to eliminate recursive application
+    _root_.f x
+
 
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
@@ -22,12 +26,12 @@ f.g : Nat → Nat
 terminationFailure.lean:20:4-20:5: error: fail to show termination for
   h
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Cannot use parameter x:
   failed to eliminate recursive application
     h x
 
+
 failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
diff --git a/tests/lean/wf1.lean.expected.out b/tests/lean/wf1.lean.expected.out
index 116ef8c5c0..3d1f386297 100644
--- a/tests/lean/wf1.lean.expected.out
+++ b/tests/lean/wf1.lean.expected.out
@@ -1,16 +1,15 @@
 wf1.lean:1:4-1:5: error: fail to show termination for
   g
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Cannot use parameter x:
   failed to eliminate recursive application
     g (x - 1)
-
-argument #2 cannot be used for structural recursion
+Cannot use parameter y:
   insufficient number of parameters at recursive application 
     g (x - 1)
 
+
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)