diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 5a328e9cd8..551aa09b6a 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -9,6 +9,10 @@ namespace Lean
 namespace Parser
 namespace Tactic
 
+-- Auxiliary parsing category just to expose the nonterminal `tacticSeq` to the `syntax` command
+builtin_initialize
+  registerBuiltinParserAttribute `builtinTacticSeqParser `tacticSeq
+
 def underscoreFn : ParserFn := fun c s =>
   let s   := symbolFn "_" c s;
   let stx := s.stxStack.back;