From 188ff2dd2026bcdea384f54f519d32567cd4df98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 30 Dec 2023 16:15:05 -0800
Subject: [PATCH] chore: remove bogus `registerSimproc`

---
 src/Lean/Elab/Tactic/Simproc.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Simproc.lean b/src/Lean/Elab/Tactic/Simproc.lean
index 2905d87f2d..e7c3f21707 100644
--- a/src/Lean/Elab/Tactic/Simproc.lean
+++ b/src/Lean/Elab/Tactic/Simproc.lean
@@ -46,7 +46,6 @@ namespace Command
   liftTermElabM do
     checkSimprocType declName
     let keys ← elabSimprocKeys pattern
-    registerSimproc declName keys
     let val := mkAppN (mkConst ``registerBuiltinSimproc) #[toExpr declName, toExpr keys]
     let initDeclName ← mkFreshUserName (declName ++ `declare)
     declareBuiltin initDeclName val