diff --git a/src/Lean/Meta/CollectFVars.lean b/src/Lean/Meta/CollectFVars.lean
index ce47dfd828..cec47b6086 100644
--- a/src/Lean/Meta/CollectFVars.lean
+++ b/src/Lean/Meta/CollectFVars.lean
@@ -21,11 +21,6 @@ def LocalDecl.collectFVars (localDecl : LocalDecl) : StateRefT CollectFVars.Stat
 
 namespace Meta
 
-def collectUsedFVarsAtFVars (fvars : Array Expr) : StateRefT CollectFVars.State MetaM Unit :=
-  fvars.forM fun fvar => do
-    let fvarType ← inferType fvar
-    fvarType.collectFVars
-
 def removeUnused (vars : Array Expr) (used : CollectFVars.State) : MetaM (LocalContext × LocalInstances × Array Expr) := do
   let localInsts ← getLocalInstances
   let lctx ← getLCtx