src/ZF/Tools/datatype_package.ML
changeset 22101 6d13239d5f52
parent 21350 6e58289b6685
child 22578 b0eb5652f210
--- a/src/ZF/Tools/datatype_package.ML	Fri Jan 19 22:08:07 2007 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Fri Jan 19 22:08:08 2007 +0100
@@ -417,9 +417,9 @@
 val datatype_decl =
   (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
   P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
-  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
-  Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] --
-  Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) []
+  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
+  Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
+  Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
   >> (Toplevel.theory o mk_datatype);
 
 val coind_prefix = if coind then "co" else "";