| changeset 6729 | b6e167580a32 |
| parent 6723 | f342449d73ca |
| child 6851 | 526c0b90bcef |
--- a/src/HOL/Tools/record_package.ML Tue May 25 20:23:30 1999 +0200 +++ b/src/HOL/Tools/record_package.ML Tue May 25 20:24:10 1999 +0200 @@ -882,7 +882,7 @@ val record_decl = P.type_args -- P.name -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") - -- Scan.repeat1 (P.name -- (P.$$$ "::" |-- P.typ))); + -- Scan.repeat1 (P.name -- (P.$$$ "::" |-- P.typ) --| P.marg_comment)); val recordP = OuterSyntax.command "record" "define extensible record" K.thy_decl