--- a/src/ZF/Tools/datatype_package.ML Fri Nov 16 22:08:28 2001 +0100
+++ b/src/ZF/Tools/datatype_package.ML Fri Nov 16 22:08:55 2001 +0100
@@ -419,10 +419,10 @@
val con_decl =
P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
- >> P.triple1;
+ --| P.marg_comment >> P.triple1;
val datatype_decl =
- (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
+ (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term --| P.marg_comment) "") --
P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] --