diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 7585f4b970..71d3911341 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/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
diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index ec5688e5ee..2fefbb0f3b 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/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
diff --git a/src/Lean/Elab/PreDefinition/Structural/Basic.lean b/src/Lean/Elab/PreDefinition/Structural/Basic.lean
index 6d0862783a..14bbb60b73 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Basic.lean
+++ b/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
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 7c8afca239..5a482d4aa2 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/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` -/