--- a/src/ZF/Tools/datatype_package.ML Thu Aug 21 13:46:29 2014 +0200
+++ b/src/ZF/Tools/datatype_package.ML Thu Aug 21 22:48:39 2014 +0200
@@ -437,9 +437,9 @@
("define " ^ coind_prefix ^ "datatype")
((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
- Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
- Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
- Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
+ Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
+ Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
>> (Toplevel.theory o mk_datatype));
end;