diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 2a3c1758c0..a62107e949 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -98,8 +98,8 @@ syntax calcStep := colGe term " := " withPosition(term)
 syntax "calc " withPosition(calcStep+) : term
 
 macro_rules
-  | `(calc $p:term := $h:term) => `(($h : $p))
-  | `(calc $p:term := $h:term $rest:calcStep*) => ``(trans ($h : $p) (calc $rest:calcStep*))
+  | `(calc $p:term := $h:term) => `(show $p from $h)
+  | `(calc $p:term := $h:term $rest:calcStep*) => ``(trans (show $p from $h) (calc $rest:calcStep*))
 
 @[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
diff --git a/tests/lean/run/calcBug.lean b/tests/lean/run/calcBug.lean
new file mode 100644
index 0000000000..f04caf586b
--- /dev/null
+++ b/tests/lean/run/calcBug.lean
@@ -0,0 +1,15 @@
+namespace Hidden
+
+open Nat
+
+theorem zero_add (n : Nat) : 0 + n = n :=
+  Nat.recOn (motive := fun x => 0 + x = x)
+   n
+   (show 0 + 0 = 0 from rfl)
+   (fun (n : Nat) (ih : 0 + n = n) =>
+    show 0 + succ n = succ n from
+    calc
+       0 + succ n = succ (0 + n) := rfl
+                _ = succ n       := by rw [ih])
+
+end Hidden