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