# HG changeset patch
# User wenzelm
# Date 1005944935 -3600
# Node ID 0474ed2b23aae47a47201a1cd61260014a121c5e
# Parent  2d5b513199da146d76b1d8f749336d2e1eb3369b
additional P.marg_comment;

diff -r 2d5b513199da -r 0474ed2b23aa src/ZF/Tools/datatype_package.ML
--- 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) [] --