From fd0a209f7425f021d110c9469aac62434ec63367 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 10 Nov 2023 17:17:27 +0100
Subject: [PATCH] refactor: TerminationHint: Remove duplicted code line (#2859)

(I sincerely hope that erasing from a map is idempotent :-))
---
 src/Lean/Elab/PreDefinition/WF/TerminationHint.lean | 1 -
 1 file changed, 1 deletion(-)

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