--- a/src/ZF/Tools/datatype_package.ML Wed Apr 13 17:00:02 2016 +0200
+++ b/src/ZF/Tools/datatype_package.ML Wed Apr 13 18:01:05 2016 +0200
@@ -433,9 +433,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.xthms1) [] --
- Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
- Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) [] --
+ Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.thms1) [] --
+ Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.thms1) []
>> (Toplevel.theory o mk_datatype));
end;