diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index 5000a451cb..29ed50bb2f 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -127,4 +127,9 @@ theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
 theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
   Decidable.byContradiction (dec := propDecidable _) h
 
+macro "byCases" h:ident ":" e:term : tactic =>
+  `(cases em $e:term with
+    | Or.inl $h:ident => _
+    | Or.inr $h:ident => _)
+
 end Classical
diff --git a/tests/lean/run/ac_expr.lean b/tests/lean/run/ac_expr.lean
index b1d4ab5e9c..030b0ac71a 100644
--- a/tests/lean/run/ac_expr.lean
+++ b/tests/lean/run/ac_expr.lean
@@ -104,11 +104,6 @@ def mkExpr : List Nat → Expr
   | [i]   => Expr.var i
   | i::is => Expr.op (Expr.var i) (mkExpr is)
 
-macro "byCases" h:ident ":" e:term : tactic =>
-  `(cases Decidable.em $e:term with
-    | Or.inl $h:ident => _
-    | Or.inr $h:ident => _)
-
 theorem Expr.denote_sort (ctx : Context α) (e : Expr) : denote ctx (sort e) = denote ctx e := by
   apply denote_loop
 where