diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 63562d6d58..5b47d184f0 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -26,6 +26,7 @@ fun c s =>
 def ident' : Parser := ident <|> underscore
 
 @[builtinTacticParser] def «intro»      := parser! nonReservedSymbol "intro " >> many (termParser maxPrec)
+@[builtinTacticParser] def «introMatch» := parser! nonReservedSymbol "intro " >> Term.funMatchAlts
 @[builtinTacticParser] def «intros»     := parser! nonReservedSymbol "intros " >> many ident'
 @[builtinTacticParser] def «revert»     := parser! nonReservedSymbol "revert " >> many1 ident
 @[builtinTacticParser] def «clear»      := parser! nonReservedSymbol "clear " >> many1 ident