diff -r dc58ab4d9f44 -r e4250d370657 src/ZF/Tools/datatype_package.ML
--- 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;