From 17fa60e1ec209580db8a45066bc08da527477fbc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jun 2022 09:31:52 -0700
Subject: [PATCH] chore: remove dead code

---
 src/Lean/Meta/CollectFVars.lean | 5 -----
 1 file changed, 5 deletions(-)

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