diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
index 2538b86a97..997d068a17 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
@@ -53,7 +53,6 @@ def TerminationHint.markAsUsed (t : TerminationHint) (clique : Array Name) : Ter
   | TerminationHint.many m => Id.run do
     for declName in clique do
       if m.contains declName then
-        let m := m.erase declName
         let m := m.erase declName
         if m.isEmpty then
           return TerminationHint.none