diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index f0fc15f1aa..f4094d06ff 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -81,7 +81,7 @@ def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> def structImplicitBinder := leading_parser atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}" def structInstBinder := leading_parser atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]" def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault) -def structFields := leading_parser manyIndent (ppLine >> checkColGe >>(structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder)) +def structFields := leading_parser manyIndent (ppLine >> checkColGe >> ppGroup (structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder)) def structCtor := leading_parser atomic (declModifiers true >> ident >> optional inferMod >> " :: ") def structureTk := leading_parser "structure " def classTk := leading_parser "class "