diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean
index 1e8c799579..3cc4c8fc6e 100644
--- a/src/Init/Lean/Parser/Tactic.lean
+++ b/src/Init/Lean/Parser/Tactic.lean
@@ -42,6 +42,7 @@ def seq := parser! sepBy tacticParser "; " true
 @[builtinTacticParser] def «apply»      := parser! nonReservedSymbol "apply " >> termParser
 @[builtinTacticParser] def «exact»      := parser! nonReservedSymbol "exact " >> termParser
 @[builtinTacticParser] def «refine»     := parser! nonReservedSymbol "refine " >> termParser
+@[builtinTacticParser] def «case»       := parser! nonReservedSymbol "case " >> ident >> tacticParser
 @[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
 @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
 @[builtinTacticParser] def orelse := tparser! pushLeading >> " <|> " >> tacticParser 1