diff -r 4e4738698db4 -r 9f394a16c557 src/ZF/Tools/datatype_package.ML
--- 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;