diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 4ec4c0fb2b..3a94c14407 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -420,7 +420,7 @@ example (n : ℕ) : n = n :=
 begin
   with_cases { induction n },
   case nat.zero { reflexivity },
-  case nat.succ n' ih { reflexivity }
+  case nat.succ : n' ih { reflexivity }
 end
 ```