| changeset 6729 | b6e167580a32 |
| parent 6723 | f342449d73ca |
| child 6766 | 34270fe45516 |
--- a/src/HOL/Tools/datatype_package.ML Tue May 25 20:23:30 1999 +0200 +++ b/src/HOL/Tools/datatype_package.ML Tue May 25 20:24:10 1999 +0200 @@ -670,7 +670,7 @@ val datatype_decl = Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix -- - (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix)); + (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix --| P.marg_comment)); fun mk_datatype args = let