refactor: move and generalize ensureNoRecFn

src/Lean/Elab/PreDefinition/Basic.lean

@@ -170,4 +170,16 @@ def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit :=
           | _ => none
         modifiers := {} }
 
+private def containsRecFn (recFnName : Name) (e : Expr) : Bool :=
+  (e.find? fun e => e.isConstOf recFnName).isSome
+
+def ensureNoRecFn (recFnName : Name) (e : Expr) : MetaM Expr := do
+  if containsRecFn recFnName e then
+    Meta.forEachExpr e fun e => do
+      if e.isAppOf recFnName then
+        throwError "unexpected occurrence of recursive application{indentExpr e}"
+    pure e
+  else
+    pure e
+
 end Lean.Elab

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Match.Match
 import Lean.Elab.RecAppSyntax
+import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 
 namespace Lean.Elab.Structural

src/Lean/Elab/PreDefinition/Structural/Basic.lean

@@ -54,16 +54,4 @@ def recArgHasLooseBVarsAt (recFnName : Name) (recArgPos : Nat) (e : Expr) : Bool
      e.isAppOf recFnName && e.getAppNumArgs > recArgPos && (e.getArg! recArgPos).hasLooseBVars
   app?.isSome
 
-private def containsRecFn (recFnName : Name) (e : Expr) : Bool :=
-  (e.find? fun e => e.isConstOf recFnName).isSome
-
-def ensureNoRecFn (recFnName : Name) (e : Expr) : MetaM Expr := do
-  if containsRecFn recFnName e then
-    Meta.forEachExpr e fun e => do
-      if e.isAppOf recFnName then
-        throwError "unexpected occurrence of recursive application{indentExpr e}"
-    pure e
-  else
-    pure e
-
 end Lean.Elab.Structural

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -74,7 +74,7 @@ private partial def replaceRecApps (recFnName : Name) (decrTactic? : Option Synt
                 mkLambdaFVars xs (← loop FAlt altBody)
             return { matcherApp with alts := altsNew, discrs := (← matcherApp.discrs.mapM (loop F)) }.toExpr
       | none => processApp e
-    | e => Structural.ensureNoRecFn recFnName e
+    | e => ensureNoRecFn recFnName e
   loop F e
 
 /-- Refine `F` over `Sum.casesOn` -/