--- a/src/ZF/Tools/datatype_package.ML Sat Jan 26 17:08:43 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sat Jan 26 20:01:37 2008 +0100
@@ -413,7 +413,7 @@
>> P.triple1;
val datatype_decl =
- (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
+ (Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --