diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 46ad7afbcf..b959d68fcf 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -170,9 +170,9 @@ macro "rfl'" : tactic => `(set_option smartUnfolding false in with_unfolding_all
 syntax (name := ac_refl) "ac_refl " : tactic
 
 /-- `admit` is a shorthand for `exact sorry`. -/
-macro "admit" : tactic => `(exact sorry)
+macro "admit" : tactic => `(exact @sorryAx _ false)
 /-- The `sorry` tactic is a shorthand for `exact sorry`. -/
-macro "sorry" : tactic => `(exact sorry)
+macro "sorry" : tactic => `(exact @sorryAx _ false)
 /-- `infer_instance` is an abbreviation for `exact inferInstance` -/
 macro "infer_instance" : tactic => `(exact inferInstance)
 
diff --git a/tests/lean/run/1230.lean b/tests/lean/run/1230.lean
new file mode 100644
index 0000000000..61ab14a5f3
--- /dev/null
+++ b/tests/lean/run/1230.lean
@@ -0,0 +1,3 @@
+example: ∀ {t}, 0 ≤ t := by
+  have : True := trivial
+  sorry