diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index fc1b88d8cd..b7a3a7a962 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -368,13 +368,13 @@ private def checkResultingUniverses (indTypes : List InductiveType) : TermElabM
 
 private def collectUsed (indTypes : List InductiveType) : StateRefT CollectFVars.State MetaM Unit := do
   indTypes.forM fun indType => do
-    Term.collectUsedFVars indType.type
+    Meta.collectUsedFVars indType.type
     indType.ctors.forM fun ctor =>
-      Term.collectUsedFVars ctor.type
+      Meta.collectUsedFVars ctor.type
 
 private def removeUnused (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (LocalContext × LocalInstances × Array Expr) := do
   let (_, used) ← (collectUsed indTypes).run {}
-  Term.removeUnused vars used
+  Meta.removeUnused vars used
 
 private def withUsed {α} (vars : Array Expr) (indTypes : List InductiveType) (k : Array Expr → TermElabM α) : TermElabM α := do
   let (lctx, localInsts, vars) ← removeUnused vars indTypes
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 644bdab741..cf60a36fa7 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -588,18 +588,18 @@ private def getResultUniverse (type : Expr) : TermElabM Level := do
 private def collectUsed (params : Array Expr) (fieldInfos : Array StructFieldInfo) : StateRefT CollectFVars.State MetaM Unit := do
   params.forM fun p => do
     let type ← inferType p
-    Term.collectUsedFVars type
+    Meta.collectUsedFVars type
   fieldInfos.forM fun info => do
     let fvarType ← inferType info.fvar
-    Term.collectUsedFVars fvarType
+    Meta.collectUsedFVars fvarType
     match info.value? with
     | none       => pure ()
-    | some value => Term.collectUsedFVars value
+    | some value => Meta.collectUsedFVars value
 
 private def removeUnused (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
     : TermElabM (LocalContext × LocalInstances × Array Expr) := do
   let (_, used) ← (collectUsed params fieldInfos).run {}
-  Term.removeUnused scopeVars used
+  Meta.removeUnused scopeVars used
 
 private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (k : Array Expr → TermElabM α)
     : TermElabM α := do
diff --git a/src/Lean/Meta/CollectFVars.lean b/src/Lean/Meta/CollectFVars.lean
index 7ebaab9772..e3a2aa15f9 100644
--- a/src/Lean/Meta/CollectFVars.lean
+++ b/src/Lean/Meta/CollectFVars.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 import Lean.Util.CollectFVars
 import Lean.Elab.Term
 
-namespace Lean.Elab.Term
+namespace Lean.Meta
 open Meta
 
 def collectUsedFVars (e : Expr) : StateRefT CollectFVars.State MetaM Unit := do
@@ -22,8 +22,7 @@ def removeUnused (vars : Array Expr) (used : CollectFVars.State) : MetaM (LocalC
   let localInsts ← getLocalInstances
   let lctx ← getLCtx
   let (lctx, localInsts, newVars, _) ← vars.foldrM
-    (fun var (result : LocalContext × LocalInstances × Array Expr × CollectFVars.State) => do
-      let (lctx, localInsts, newVars, used) := result
+    (fun var (lctx, localInsts, newVars, used) => do
       if used.fvarSet.contains var.fvarId! then
         let varType ← inferType var
         let (_, used) ← (collectUsedFVars varType).run used
@@ -33,4 +32,4 @@ def removeUnused (vars : Array Expr) (used : CollectFVars.State) : MetaM (LocalC
     (lctx, localInsts, #[], used)
   pure (lctx, localInsts, newVars.reverse)
 
-end Lean.Elab.Term
+end Lean.Meta