diff -r bda60442bf02 -r a70df1e5bf10 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Feb 12 20:25:58 2002 +0100
+++ b/src/HOL/Tools/record_package.ML	Tue Feb 12 20:28:27 2002 +0100
@@ -1086,8 +1086,8 @@
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
 val record_decl =
-  P.type_args -- P.name -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+")
-    -- Scan.repeat1 (P.const --| P.marg_comment));
+  P.type_args -- P.name --
+    (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
 
 val recordP =
   OuterSyntax.command "record" "define extensible record" K.thy_decl