diff --git a/src/Lean/Meta/CollectFVars.lean b/src/Lean/Meta/CollectFVars.lean
index 8f8eb71ae6..d4bafed016 100644
--- a/src/Lean/Meta/CollectFVars.lean
+++ b/src/Lean/Meta/CollectFVars.lean
@@ -34,13 +34,8 @@ where
     else
       return none
 
-  alreadyVisited (fvarId : FVarId) : StateRefT Nat (StateRefT CollectFVars.State MetaM) Bool := do
-    let s ← getThe CollectFVars.State
-    return s.visitedExpr.contains (mkFVar fvarId)
-
   go : StateRefT Nat (StateRefT CollectFVars.State MetaM) Unit := do
     let some fvarId ← getNext? | return ()
-    if (← alreadyVisited fvarId) then return ()
     /- We don't use `getLocalDecl` because `CollectFVars.State` may contains local variables that are not in the
        current local context. Recall that we use this method to process match-expressions, and each AltLHS has
        each own its extra local declarations. -/
diff --git a/tests/lean/run/1247.lean b/tests/lean/run/1247.lean
new file mode 100644
index 0000000000..680ddd71a2
--- /dev/null
+++ b/tests/lean/run/1247.lean
@@ -0,0 +1,8 @@
+inductive TestResult (p : Prop) where
+  | success : TestResult p
+
+abbrev DecorationsOf (p : Prop) := Prop
+
+def check (p' : DecorationsOf p) (x : TestResult p') : Unit :=
+  match x with
+  | .success => ()