src/HOL/Tools/old_inductive_package.ML
changeset 22101 6d13239d5f52
parent 21879 a3efbae45735
child 22846 fb79144af9a3
--- a/src/HOL/Tools/old_inductive_package.ML	Fri Jan 19 22:08:07 2007 +0100
+++ b/src/HOL/Tools/old_inductive_package.ML	Fri Jan 19 22:08:08 2007 +0100
@@ -888,8 +888,8 @@
 fun ind_decl coind =
   Scan.repeat1 P.term --
   (P.$$$ "intros" |--
-    P.!!! (Scan.repeat (P.opt_thm_name ":" -- P.prop))) --
-  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
+    P.!!! (Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop))) --
+  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
   >> (Toplevel.theory o mk_ind coind);
 
 val inductiveP =
@@ -900,7 +900,7 @@
 
 
 val ind_cases =
-  P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
+  P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
   >> (Toplevel.theory o inductive_cases);
 
 val inductive_casesP =