diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index ad3ead505f..f4018ac34f 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -311,6 +311,12 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
           | false, true  => `(Parser.Tactic.simpLemma| ↓ ← $decl:term)
           | false, false => `(Parser.Tactic.simpLemma| ↓ $decl:term)
         args := args.push arg
+      else if (← Simp.isBuiltinSimproc declName) then
+        let decl := mkIdent declName
+        let arg ← match post with
+          | true  => `(Parser.Tactic.simpLemma| $decl:term)
+          | false => `(Parser.Tactic.simpLemma| ↓ $decl:term)
+        args := args.push arg
     | .fvar fvarId => -- local hypotheses in the context
       -- `simp_all` always uses all propositional hypotheses (and it can't use
       -- any others). So `simp_all only [h]`, where `h` is a hypothesis, would
diff --git a/tests/lean/builtinSimprocTrace.lean b/tests/lean/builtinSimprocTrace.lean
new file mode 100644
index 0000000000..73d656ae85
--- /dev/null
+++ b/tests/lean/builtinSimprocTrace.lean
@@ -0,0 +1,6 @@
+def f (_ : Nat) := 10
+
+set_option tactic.simp.trace true
+example : f x = (if true then 8 + 2 else 0) := by
+ simp
+ rw [f]
diff --git a/tests/lean/builtinSimprocTrace.lean.expected.out b/tests/lean/builtinSimprocTrace.lean.expected.out
new file mode 100644
index 0000000000..6439001ea8
--- /dev/null
+++ b/tests/lean/builtinSimprocTrace.lean.expected.out
@@ -0,0 +1 @@
+Try this: simp only [↓reduceIte, Nat.reduceAdd]