diff --git a/src/Lean/Elab/Tactic/Simproc.lean b/src/Lean/Elab/Tactic/Simproc.lean
index 1e81605167..91caacec0e 100644
--- a/src/Lean/Elab/Tactic/Simproc.lean
+++ b/src/Lean/Elab/Tactic/Simproc.lean
@@ -46,7 +46,7 @@ namespace Command
   liftTermElabM do
     checkSimprocType declName
     let keys ← elabSimprocKeys pattern
-    let val := mkAppN (mkConst ``registerBuiltinSimprocNew) #[toExpr declName, toExpr keys, mkConst declName]
+    let val := mkAppN (mkConst ``registerBuiltinSimproc) #[toExpr declName, toExpr keys, mkConst declName]
     let initDeclName ← mkFreshUserName (declName ++ `declare)
     declareBuiltin initDeclName val
 
diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean
index 01df8e086a..1303d5cda3 100644
--- a/src/Lean/Meta/Tactic/Simp/Simproc.lean
+++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean
@@ -59,13 +59,13 @@ def isBuiltinSimproc (declName : Name) : CoreM Bool := do
 def isSimproc (declName : Name) : CoreM Bool :=
   return (← getSimprocDeclKeys? declName).isSome
 
-def registerBuiltinSimproc (declName : Name) (key : Array SimpTheoremKey) : IO Unit := do
+def registerBuiltinSimproc (declName : Name) (key : Array SimpTheoremKey) (proc : Simproc) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError s!"invalid builtin simproc declaration, it can only be registered during initialization")
   if (← builtinSimprocDeclsRef.get).keys.contains declName then
     throw (IO.userError s!"invalid builtin simproc declaration '{declName}', it has already been declared")
   builtinSimprocDeclsRef.modify fun { keys, procs } =>
-    { keys := keys.insert declName key, procs }
+    { keys := keys.insert declName key, procs := procs.insert declName proc }
 
 def registerBuiltinSimprocNew (declName : Name) (key : Array SimpTheoremKey) (proc : Simproc) : IO Unit := do
   unless (← initializing) do