diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index f7542d9787..24e63dca8a 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -123,11 +123,11 @@ partial def toBelow (below : Expr) (numIndParams : Nat) (positions : Positions)
       toBelowAux Cs[fnIndex]! belowDict recArg below
 
 private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : Positions)
-    (below : Expr) (e : Expr) : M Expr :=
+    (below : Expr) (e : Expr) : MetaM Expr :=
   let recFnNames := recArgInfos.map (·.fnName)
-  let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) M Bool :=
+  let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) MetaM Bool :=
     modifyGet (HasConstCache.contains e |>.run ·)
-  let rec loop (below : Expr) (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr := do
+  let rec loop (below : Expr) (e : Expr) : StateRefT (HasConstCache recFnNames) MetaM Expr := do
     if !(← containsRecFn e) then
       return e
     match e with
@@ -147,7 +147,7 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions :
         return mkMData d (← loop below b)
     | Expr.proj n i e => return mkProj n i (← loop below e)
     | Expr.app _ _ =>
-      let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr :=
+      let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) MetaM Expr :=
         e.withApp fun f args => do
           if let .some fnIdx := recArgInfos.findFinIdx? (f.isConstOf ·.fnName) then
             let recArgInfo := recArgInfos[fnIdx]
@@ -208,10 +208,11 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions :
 /--
 Calculates the `.brecOn` motive corresponding to one structural recursive function.
 The `value` is the function with (only) the fixed parameters moved into the context.
+The `type` is the corresponding function type with (only) the fixed parameters instantiated.
 -/
-def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
-  lambdaTelescope value fun xs value => do
-    let type  := (← inferType value).headBeta
+def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) (type : Expr) : MetaM Expr := do
+  lambdaTelescope value fun xs _value => do
+    let type ← instantiateForall type xs
     let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
     let motive ← mkForallFVars otherArgs type
     mkLambdaFVars indexMajorArgs motive
@@ -224,7 +225,7 @@ The `recArgInfos` is used to transform the body of the function to replace recur
 uses of the `below` induction hypothesis.
 -/
 def mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
-    (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : M Expr := do
+    (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : MetaM Expr := do
   lambdaTelescope value fun xs value => do
     let (indicesMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
     let FType ← instantiateForall FType indicesMajorArgs
diff --git a/src/Lean/Elab/PreDefinition/Structural/Basic.lean b/src/Lean/Elab/PreDefinition/Structural/Basic.lean
index 3483eedf14..b576b473a8 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Basic.lean
@@ -12,22 +12,6 @@ public section
 
 namespace Lean.Elab.Structural
 
-structure State where
-  /-- As part of the inductive predicates case, we keep adding more and more discriminants from the
-     local context and build up a bigger matcher application until we reach a fixed point.
-     As a side-effect, this creates matchers. Here we capture all these side-effects, because
-     the construction rolls back any changes done to the environment and the side-effects
-     need to be replayed. -/
-  addMatchers : Array (MetaM Unit) := #[]
-
-abbrev M := StateRefT State MetaM
-
-instance : Inhabited (M α) where
-  default := throwError "failed"
-
-def run (x : M α) (s : State := {}) : MetaM (α × State) :=
-  StateRefT'.run x s
-
 /--
   Return true iff `e` contains an application `recFnName .. t ..` where the term `t` is
   the argument we are trying to recurse on, and it contains loose bound variables.
diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
index 4becbfe978..92802d1641 100644
--- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
@@ -235,9 +235,27 @@ def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
     some (go 0 #[])
 
 
-def tryAllArgs (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
-   (values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) : M α := do
+/-- A candidate argument combination to try for structural recursion. -/
+structure RecArgCandidate where
+  group : IndGroupInst
+  comb : Array RecArgInfo
+
+/-- Result of `findRecArgCandidates`: candidate combinations and a diagnostic report. -/
+structure RecArgCandidates where
+  candidates : Array RecArgCandidate
+  report : MessageData
+
+/--
+Precompute all candidate argument combinations for structural recursion.
+This performs the analysis that may need function axioms in the environment
+(via `isDefEq`, `inferType`, etc.) but does not run the callback that
+attempts to eliminate mutual recursion.
+-/
+def findRecArgCandidates (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
+    (values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) :
+    MetaM RecArgCandidates := do
   let mut report := m!""
+  let mut candidates := #[]
   -- Gather information on all possible recursive arguments
   let mut recArgInfoss := #[]
   for fnName in fnNames, value in values, termMeasure? in termMeasure?s, fixedParamPerm in fixedParamPerms.perms do
@@ -263,23 +281,30 @@ def tryAllArgs (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs :
       continue
     if let some combs := allCombinations recArgInfoss' then
       for comb in combs do
-        try
-          -- Check that the group actually has a brecOn (we used to check this in getRecArgInfo,
-          -- but in the first phase we do not want to rule-out non-recursive types like `Array`, which
-          -- are ok in a nested group. This logic can maybe simplified)
-          unless (← hasConst (group.brecOnName 0)) do
-            throwError "the type {group} does not have a `.brecOn` recursor"
-          let r ← k comb
-          trace[Elab.definition.structural] "tryAllArgs report:\n{report}"
-          return r
-        catch e =>
-          let m ← prettyParameterSet fnNames xs values comb
-          report := report ++ m!"Cannot use {m}:{indentD e.toMessageData}\n"
+        candidates := candidates.push { group, comb }
     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 := report ++ m!"Too many possible combinations of parameters of type {group} (or " ++
+        m!"please indicate the recursive argument explicitly using `termination_by structural`).\n"
+  return { candidates, report }
+
+/--
+Try each candidate argument combination for structural recursion.
+Uses `commitIfNoEx` to backtrack on failure.
+-/
+def tryCandidates (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
+    (candidates : RecArgCandidates) (k : Array RecArgInfo → MetaM α) : MetaM α := do
+  let mut report := candidates.report
+  for candidate in candidates.candidates do
+    try
+      return ← commitIfNoEx do
+        unless (← hasConst (candidate.group.brecOnName 0)) do
+          throwError "the type {candidate.group} does not have a `.brecOn` recursor"
+        k candidate.comb
+    catch e =>
+      let m ← prettyParameterSet fnNames xs values candidate.comb
+      report := report ++ m!"Cannot use {m}:{indentD e.toMessageData}\n"
   report := m!"failed to infer structural recursion:\n" ++ report
-  trace[Elab.definition.structural] "tryAllArgs:\n{report}"
+  trace[Elab.definition.structural] "tryCandidates:\n{report}"
   throwError report
 
 end Lean.Elab.Structural
diff --git a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
index 463c850993..9e4c0a308e 100644
--- a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
@@ -43,12 +43,15 @@ def replaceIndPredRecApp (recArgInfo : RecArgInfo) (ctx : RecursionContext) (fid
   let recApp := andProj pos positions[motiveIdx]!.size recApp
   return mkAppN recApp ys
 
+/-- Monad for inductive predicate recursion that accumulates matcher creation side-effects. -/
+private abbrev IndPredM := StateRefT (Array (MetaM Unit)) MetaM
+
 partial def replaceIndPredRecApps (recArgInfos : Array RecArgInfo) (positions : Positions)
-    (params : Array Expr) (ctx : RecursionContext) (e : Expr) : M Expr := do
+    (params : Array Expr) (ctx : RecursionContext) (e : Expr) : IndPredM Expr := do
   let recFnNames := recArgInfos.map (·.fnName)
-  let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) M Bool :=
+  let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) IndPredM Bool :=
     modifyGet (·.contains e)
-  let rec loop (ctx : RecursionContext) (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr := do
+  let rec loop (ctx : RecursionContext) (e : Expr) : StateRefT (HasConstCache recFnNames) IndPredM Expr := do
     unless ← containsRecFn e do
       return e
     match e with
@@ -68,7 +71,7 @@ partial def replaceIndPredRecApps (recArgInfos : Array RecArgInfo) (positions :
         return e.updateMData! (← loop ctx b)
     | .proj _ _ e' => return e.updateProj! (← loop ctx e')
     | .app _ _ =>
-      let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr := do
+      let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) IndPredM Expr := do
         e.withApp fun f args => do
           let args ← args.mapM (loop ctx)
           if let .const c _ := f then
@@ -84,7 +87,7 @@ partial def replaceIndPredRecApps (recArgInfos : Array RecArgInfo) (positions :
         IndPredBelow.mkBelowMatcher matcherApp params nrealParams ctx fun ctx e =>
           g (loop ctx e)
       if let some (newApp, addMatcher) := matcherResult then
-        modifyThe State fun s => { s with addMatchers := s.addMatchers.push addMatcher }
+        modifyThe (Array (MetaM Unit)) (·.push addMatcher)
         processApp newApp -- recursive applications may still be hidden in e.g. the discriminants
       else
         -- Note: `recArgHasLooseBVarsAt` has false positives, so sometimes everything might stay
@@ -99,10 +102,10 @@ partial def replaceIndPredRecApps (recArgInfos : Array RecArgInfo) (positions :
 Turns `fun a b => x` into `let funType := fun a b => α` (where `x : α`).
 The continuation is the called with all `funType`s corresponding to the values.
 -/
-public def withFunTypes (values : Array Expr) (k : Array Expr → M α) : M α := do
+public def withFunTypes (values : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do
   go 0 #[]
 where
-  go (i : Nat) (res : Array Expr) : M α :=
+  go (i : Nat) (res : Array Expr) : MetaM α :=
     if h : i < values.size then
       lambdaTelescope values[i] fun xs value => do
         let type := (← inferType value).headBeta
@@ -117,7 +120,7 @@ where
 Calculates the `.brecOn` motive corresponding to one structural recursive function.
 The `value` is the function with (only) the fixed parameters moved into the context.
 -/
-public def mkIndPredBRecOnMotive (recArgInfo : RecArgInfo) (value funType : Expr) : M Expr := do
+public def mkIndPredBRecOnMotive (recArgInfo : RecArgInfo) (value funType : Expr) : MetaM Expr := do
   lambdaTelescope value fun xs _ => do
     let type := mkAppN funType xs
     let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
@@ -130,9 +133,12 @@ The `value` is the function with (only) the fixed parameters moved into the cont
 The `FType` is the expected type of the argument.
 The `recArgInfos` is used to transform the body of the function to replace recursive calls with
 uses of the `below` induction hypothesis.
+Returns the functional argument and any matchers that were created as side effects.
+The matchers are created inside `withoutModifyingEnv` and need to be replayed afterwards.
 -/
 public def mkIndPredBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
-    (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) (params : Array Expr) : M Expr := do
+    (recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) (params : Array Expr) :
+    MetaM (Expr × Array (MetaM Unit)) := do
   lambdaTelescope value fun xs value => do
     let (indicesMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
     let FType ← instantiateForall FType indicesMajorArgs
@@ -143,8 +149,9 @@ public def mkIndPredBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positi
         belows := .insert {} indicesMajorArgs.back!.fvarId! (belowName, below)
         motives := {}
       }
-      let valueNew ← withDeclNameForAuxNaming recArgInfo.fnName <|
-        replaceIndPredRecApps recArgInfos positions params ctx value
-      mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
+      let (valueNew, matchers) ← (withDeclNameForAuxNaming recArgInfo.fnName <|
+        replaceIndPredRecApps recArgInfos positions params ctx value).run #[]
+      let expr ← mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
+      return (expr, matchers)
 
 end Lean.Elab.Structural
diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean
index 770636e8fa..3196ac7555 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean
@@ -21,9 +21,25 @@ namespace Lean.Elab
 namespace Structural
 open Meta
 
+/--
+Temporarily adds the recursive functions as axioms to the environment and runs the given action.
+The environment is restored afterwards, so no persistent changes (e.g. auxiliary definitions) can
+be made inside the action.
+
+This is needed around any `MetaM` code that may try to infer the type of, or unfold, expressions
+that still mention the recursive function constants (e.g. `isDefEq`, `inferType`, `whnf` on
+arguments of recursive calls). Without these axioms, the kernel would reject the unknown constants.
+-/
+private def withRecFunsAsAxioms [Monad n] [MonadLiftT MetaM n] [MonadEnv n] [MonadFinally n]
+    (preDefs : Array PreDefinition) (k : n α) : n α :=
+  withoutModifyingEnv do
+    preDefs.forM (liftM <| addAsAxiom ·)
+    k
+
 private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms)
-    (xs : Array Expr) (recArgInfos : Array RecArgInfo) : M (Array PreDefinition) := do
+    (xs : Array Expr) (recArgInfos : Array RecArgInfo) : MetaM (Array PreDefinition) := do
   let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
+  let fnTypes ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateForall ·.type xs)
   let indInfo ← getConstInfoInduct recArgInfos[0]!.indGroupInst.all[0]!
 
   -- Groups the (indices of the) definitions by their position in indInfo.all
@@ -32,15 +48,16 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
 
   let isIndPred ← isInductivePredicate indInfo.name
 
-  let withFunTypesAndMotives (k : Array Expr → Array Expr → M (Array PreDefinition)) :
-      M (Array PreDefinition) := do
+  let withFunTypesAndMotives (k : Array Expr → Array Expr → MetaM (Array PreDefinition)) :
+      MetaM (Array PreDefinition) := do
     if isIndPred then
       withFunTypes values fun funTypes => do
         let motives ← recArgInfos.mapIdxM fun idx r =>
           mkIndPredBRecOnMotive r values[idx]! funTypes[idx]!
         k funTypes motives
     else
-      let motives ← recArgInfos.zipWithM (bs := values) fun r v => mkBRecOnMotive r v
+      let motives ← recArgInfos.mapIdxM fun idx r =>
+        mkBRecOnMotive r values[idx]! fnTypes[idx]!
       k #[] motives
   withFunTypesAndMotives fun funTypes motives => do
   trace[Elab.definition.structural] "funTypes: {funTypes}, motives: {motives}"
@@ -49,13 +66,19 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
   let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
   trace[Elab.definition.structural] "FTypes: {FTypes}"
 
+  -- `withRecFunsAsAxioms` is needed for `replaceRecApps`/`replaceIndPredRecApps` which transform
+  -- recursive calls in the function body.
+  -- For inductive predicates, `mkIndPredBRecOnF` additionally creates matchers as side effects
+  -- (inside `withoutModifyingEnv`); these are replayed immediately after.
   let FArgs ← recArgInfos.mapIdxM fun idx r =>
-    let v := values[idx]!
-    let t := FTypes[idx]!
-    if isIndPred then
-      mkIndPredBRecOnF recArgInfos positions r v t (brecOnConst 0).getAppArgs
+    if isIndPred then do
+      let (fArg, matchers) ← withRecFunsAsAxioms preDefs do
+        mkIndPredBRecOnF recArgInfos positions r values[idx]! FTypes[idx]! (brecOnConst 0).getAppArgs
+      matchers.forM (·)
+      return fArg
     else
-      mkBRecOnF recArgInfos positions r v t
+      withRecFunsAsAxioms preDefs do
+        mkBRecOnF recArgInfos positions r values[idx]! FTypes[idx]!
   trace[Elab.definition.structural] "FArgs: {FArgs}"
   let brecOn := brecOnConst 0
   -- the indices and the major premise are not mentioned in the minor premises
@@ -74,50 +97,54 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
       -- NB: Do not eta-contract here, other code (e.g. FunInd) expects this to have the
       -- same number of head lambdas as the original definition
       mkLambdaFVars (fixedParamPerms.perms[i]!.buildArgs xs ys) (valueNew.beta ys)
-  return preDefs.zipWith (bs := valuesNew) fun preDef valueNew => { preDef with value := valueNew }
+  return preDefs.zipWith (bs := valuesNew) fun preDef valueNew =>
+    { preDef with value := valueNew }
 
 private def inferRecArgPos (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) :
-    M (Array Nat × Array PreDefinition × FixedParamPerms) := do
-  withoutModifyingEnv do
-    preDefs.forM (addAsAxiom ·)
-    let fnNames := preDefs.map (·.declName)
-    let numSectionVars := preDefs[0]!.numSectionVars
-    let preDefs ← preDefs.mapM fun preDef =>
+    MetaM (Array Nat × Array PreDefinition × FixedParamPerms) := do
+  let fnNames := preDefs.map (·.declName)
+  let numSectionVars := preDefs[0]!.numSectionVars
+  let preDefs ← withRecFunsAsAxioms preDefs do
+    preDefs.mapM fun preDef =>
       return { preDef with value := (← preprocess preDef.value fnNames numSectionVars) }
-    -- The syntactically fixed arguments
-    let fixedParamPerms ← getFixedParamPerms preDefs
+  let fixedParamPerms ← withRecFunsAsAxioms preDefs do
+    getFixedParamPerms preDefs
 
-    fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun xs => do
-      let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
+  fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun xs => do
+    let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
 
-      tryAllArgs fnNames fixedParamPerms xs values termMeasure?s fun recArgInfos => do
-        let recArgPoss := recArgInfos.map (·.recArgPos)
-        trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
-        let (fixedParamPerms', xs', toErase) := fixedParamPerms.erase xs (recArgInfos.map (·.indicesAndRecArgPos))
-        -- We may have to turn some fixed parameters into varying parameters
-        let recArgInfos := recArgInfos.mapIdx fun i recArgInfo =>
-          {recArgInfo with fixedParamPerm := fixedParamPerms'.perms[i]!}
-        if xs'.size != xs.size then
-          trace[Elab.definition.structural] "Reduced fixed params from {xs} to {xs'}, erasing {toErase.map mkFVar}"
-          trace[Elab.definition.structural] "New recArgInfos {repr recArgInfos}"
-        -- Check that the parameters of the IndGroupInsts are still fine
-          for recArgInfo in recArgInfos do
-            for indParam in recArgInfo.indGroupInst.params do
-              for y in toErase do
-                if (← dependsOn indParam y) then
-                  if indParam.isFVarOf y then
-                    throwError "its type is an inductive datatype and the datatype parameter\
-                      {indentExpr indParam}\n\
-                      which cannot be fixed as it is an index or depends on an index, and indices \
-                      cannot be fixed parameters when using structural recursion."
-                  else
-                    throwError "its type is an inductive datatype and the datatype parameter\
-                      {indentExpr indParam}\ndepends on the function parameter{indentExpr (mkFVar y)}\n\
-                      which cannot be fixed as it is an index or depends on an index, and indices \
-                      cannot be fixed parameters when using structural recursion."
-        withErasedFVars toErase do
-          let preDefs' ← elimMutualRecursion preDefs fixedParamPerms' xs' recArgInfos
-          return (recArgPoss, preDefs', fixedParamPerms')
+    let candidates ← withRecFunsAsAxioms preDefs do
+      findRecArgCandidates fnNames fixedParamPerms xs values termMeasure?s
+
+    -- `tryCandidates` uses `saveState`/`restoreState` to properly backtrack on failure.
+    tryCandidates fnNames xs values candidates fun recArgInfos => do
+      let recArgPoss := recArgInfos.map (·.recArgPos)
+      trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
+      let (fixedParamPerms', xs', toErase) := fixedParamPerms.erase xs (recArgInfos.map (·.indicesAndRecArgPos))
+      -- We may have to turn some fixed parameters into varying parameters
+      let recArgInfos := recArgInfos.mapIdx fun i recArgInfo =>
+        {recArgInfo with fixedParamPerm := fixedParamPerms'.perms[i]!}
+      if xs'.size != xs.size then
+        trace[Elab.definition.structural] "Reduced fixed params from {xs} to {xs'}, erasing {toErase.map mkFVar}"
+        trace[Elab.definition.structural] "New recArgInfos {repr recArgInfos}"
+      -- Check that the parameters of the IndGroupInsts are still fine
+        for recArgInfo in recArgInfos do
+          for indParam in recArgInfo.indGroupInst.params do
+            for y in toErase do
+              if (← dependsOn indParam y) then
+                if indParam.isFVarOf y then
+                  throwError "its type is an inductive datatype and the datatype parameter\
+                    {indentExpr indParam}\n\
+                    which cannot be fixed as it is an index or depends on an index, and indices \
+                    cannot be fixed parameters when using structural recursion."
+                else
+                  throwError "its type is an inductive datatype and the datatype parameter\
+                    {indentExpr indParam}\ndepends on the function parameter{indentExpr (mkFVar y)}\n\
+                    which cannot be fixed as it is an index or depends on an index, and indices \
+                    cannot be fixed parameters when using structural recursion."
+      withErasedFVars toErase do
+        let preDefsNonRec ← elimMutualRecursion preDefs fixedParamPerms' xs' recArgInfos
+        return (recArgPoss, preDefsNonRec, fixedParamPerms')
 
 def reportTermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
   if let some ref := preDef.termination.terminationBy?? then
@@ -132,10 +159,9 @@ def structuralRecursion
     (termMeasure?s : Array (Option TerminationMeasure)) :
     TermElabM Unit := do
   let names := preDefs.map (·.declName)
-  let ((recArgPoss, preDefsNonRec, fixedParamPerms), state) ← run <| inferRecArgPos preDefs termMeasure?s
+  let (recArgPoss, preDefsNonRec, fixedParamPerms) ← inferRecArgPos preDefs termMeasure?s
   for recArgPos in recArgPoss, preDef in preDefs do
     reportTermMeasure preDef recArgPos
-  state.addMatchers.forM liftM
   preDefsNonRec.forM fun preDefNonRec => do
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
     prependError m!"structural recursion failed, produced type incorrect term" do
diff --git a/tests/elab/inductive_pred.lean.out.expected b/tests/elab/inductive_pred.lean.out.expected
index c3693b9a71..a647696658 100644
--- a/tests/elab/inductive_pred.lean.out.expected
+++ b/tests/elab/inductive_pred.lean.out.expected
@@ -255,8 +255,8 @@
               n_1))
           (mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)
 [Elab.definition.structural] FArgs: [fun {m} x x_1 x_2 =>
-       @mul'.match_1_6 n funType_1 (fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m))
-         m x_2 x x_1
+       @mul'.match_1_10 n funType_1
+         (fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x_2 x x_1
          (fun h1 =>
            @of_eq_true
              (Power2
@@ -282,8 +282,8 @@
                (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n_1))
            (mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)]
 [Elab.definition.structural] packedFArgs: [fun {m} x x_1 x_2 =>
-       @mul'.match_1_6 n funType_1 (fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m))
-         m x_2 x x_1
+       @mul'.match_1_10 n funType_1
+         (fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x_2 x x_1
          (fun h1 =>
            @of_eq_true
              (Power2
@@ -308,10 +308,3 @@
              (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat)
                (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n_1))
            (mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)]
-[Elab.definition.structural] tryAllArgs report:
-    Not considering parameter n of Ex.Power2.mul':
-      it is unchanged in the recursive calls
-    Cannot use parameter #3:
-      failed to eliminate recursive application
-        @mul' n n✝ h1 h2
-