src/ZF/Tools/ind_cases.ML

--- a/src/ZF/Tools/ind_cases.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Sun May 16 00:02:11 2010 +0200
@@ -69,7 +69,7 @@
 val _ =
   OuterSyntax.command "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop)
+    (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop)
       >> (Toplevel.theory o inductive_cases));
 
 end;