Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
additional P.marg_comment;
authorwenzelm
Fri, 16 Nov 2001 22:08:55 +0100
changeset 12226 0474ed2b23aa
parent 12225 2d5b513199da
child 12227 c654c2c03f1d
additional P.marg_comment;
src/ZF/Tools/datatype_package.ML file | annotate | diff | comparison | revisions 
--- 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) [] --
isabelle