src/HOL/Tools/datatype_package.ML
changeset 22101 6d13239d5f52
parent 21772 7c7ade4f537b
child 22480 b20bc8029edb
--- a/src/HOL/Tools/datatype_package.ML	Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Jan 19 22:08:08 2007 +0100
@@ -1030,9 +1030,9 @@
 
 val rep_datatype_decl =
   Scan.option (Scan.repeat1 P.name) --
-    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
-    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
-    (P.$$$ "induction" |-- P.!!! P.xthm);
+    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
+    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
+    (P.$$$ "induction" |-- P.!!! SpecParse.xthm);
 
 fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;