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