src/ZF/Tools/ind_cases.ML

--- a/src/ZF/Tools/ind_cases.ML	Fri Jan 19 22:08:07 2007 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Fri Jan 19 22:08:08 2007 +0100
@@ -82,7 +82,7 @@
 local structure P = OuterParse and K = OuterKeyword in
 
 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 =