diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 184ebec9bb..6b0421e344 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -168,7 +168,9 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simprocs) (eras
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
             let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
-            if ctx.config.autoUnfold then
+            if (← Simp.isSimproc declName) then
+              simprocs := simprocs.erase declName
+            else if ctx.config.autoUnfold then
               thms := thms.eraseCore (.decl declName)
             else
               thms ← thms.erase (.decl declName)
diff --git a/tests/lean/run/simproc1.lean b/tests/lean/run/simproc1.lean
index 0fb409a36b..b269f4f9ac 100644
--- a/tests/lean/run/simproc1.lean
+++ b/tests/lean/run/simproc1.lean
@@ -24,3 +24,9 @@ example : x + foo 2 = 12 + x := by
   -- `simp only` does not use the default simproc set, but we can provide simprocs as arguments
   simp only [reduce_foo]
   rw [Nat.add_comm]
+
+example : x + foo 2 = 12 + x := by
+  -- We can use `-` to disable `simproc`s
+  fail_if_success simp [-reduce_foo]
+  simp
+  rw [Nat.add_comm]