diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index f78fad7b9f..a68648cdfe 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -20,8 +20,6 @@ example : True := by foo -- unknown tactic
 -/
 @[builtinTacticParser] def «unknown»    := leading_parser withPosition (ident >> errorAtSavedPos "unknown tactic" true)
 
-/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
-It runs the tactics in sequence, and fails if the goal is not solved. -/
 @[builtinTacticParser] def nestedTactic := tacticSeqBracketed
 
 def matchRhs  := Term.hole <|> Term.syntheticHole <|> tacticSeq
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 4c48c4d182..95a4f753cf 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -33,6 +33,8 @@ namespace Tactic
 
 def tacticSeq1Indented : Parser :=
   leading_parser many1Indent (group (ppLine >> tacticParser >> optional ";"))
+/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
+It runs the tactics in sequence, and fails if the goal is not solved. -/
 def tacticSeqBracketed : Parser :=
   leading_parser "{" >> many (group (ppLine >> tacticParser >> optional ";")) >> ppDedent (ppLine >> "}")
 def tacticSeq :=