diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -693,15 +693,15 @@
     val rec_name = Binding.name_of rec_binding;
     fun rec_qualified qualified = Binding.qualify qualified rec_name;
     val intr_names = map Binding.name_of intr_bindings;
-    val ind_case_names = RuleCases.case_names intr_names;
+    val ind_case_names = Rule_Cases.case_names intr_names;
     val induct =
       if coind then
-        (raw_induct, [RuleCases.case_names [rec_name],
-          RuleCases.case_conclusion (rec_name, intr_names),
-          RuleCases.consumes 1, Induct.coinduct_pred (hd cnames)])
+        (raw_induct, [Rule_Cases.case_names [rec_name],
+          Rule_Cases.case_conclusion (rec_name, intr_names),
+          Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)])
       else if no_ind orelse length cnames > 1 then
-        (raw_induct, [ind_case_names, RuleCases.consumes 0])
-      else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
+        (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
+      else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
 
     val (intrs', ctxt1) =
       ctxt |>
@@ -716,8 +716,8 @@
       LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
         LocalTheory.note kind ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
-          [Attrib.internal (K (RuleCases.case_names cases)),
-           Attrib.internal (K (RuleCases.consumes 1)),
+          [Attrib.internal (K (Rule_Cases.case_names cases)),
+           Attrib.internal (K (Rule_Cases.consumes 1)),
            Attrib.internal (K (Induct.cases_pred name)),
            Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
@@ -732,7 +732,7 @@
         LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
           inducts |> map (fn (name, th) => ([th],
             [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (RuleCases.consumes 1)),
+             Attrib.internal (K (Rule_Cases.consumes 1)),
              Attrib.internal (K (Induct.induct_pred name))])))] |> snd
       end
   in (intrs', elims', induct', ctxt3) end;