diff -r 2af1ad9aa1a3 -r ef698bd61057 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat May 15 23:40:00 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Sun May 16 00:02:11 2010 +0200
@@ -977,8 +977,8 @@
 
 fun gen_ind_decl mk_def coind =
   P.fixes -- P.for_fixes --
-  Scan.optional SpecParse.where_alt_specs [] --
-  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
+  Scan.optional Parse_Spec.where_alt_specs [] --
+  Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) []
   >> (fn (((preds, params), specs), monos) =>
       (snd oo gen_add_inductive mk_def true coind preds params specs monos));
 
@@ -995,7 +995,7 @@
 val _ =
   OuterSyntax.local_theory "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script
-    (P.and_list1 SpecParse.specs >> (snd oo inductive_cases));
+    (P.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
 
 end;