diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index b7d2141d41..d929ccb87e 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -256,7 +256,7 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar
   stx[0].getSepArgs.forM evalTactic
 
 @[builtinTactic paren] def evalParen : Tactic := fun stx =>
-  evalSeq1 stx[1]
+  evalTactic stx[1]
 
 @[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := fun stx =>
   stx[0].forArgsM fun seqElem => evalTactic seqElem[0]
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 551aa09b6a..5dc4ea9c7e 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -13,6 +13,8 @@ namespace Tactic
 builtin_initialize
   registerBuiltinParserAttribute `builtinTacticSeqParser `tacticSeq
 
+@[builtinTacticSeqParser] def tacticSeqElem := tacticSeq
+
 def underscoreFn : ParserFn := fun c s =>
   let s   := symbolFn "_" c s;
   let stx := s.stxStack.back;
@@ -79,7 +81,7 @@ def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 match
 
 def withIds : Parser := optional (" with " >> many1 (checkColGt >> ident'))
 @[builtinTacticParser] def «injection»  := parser! nonReservedSymbol "injection " >> termParser >> withIds
-@[builtinTacticParser] def paren        := parser! "(" >> seq1 >> ")"
+@[builtinTacticParser] def paren        := parser! "(" >> tacticSeq >> ")"
 @[builtinTacticParser] def nestedTactic := tacticSeqBracketed
 @[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1