diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -343,7 +343,7 @@
     Simplifier.full_simplify (HOL_basic_ss addsimprocs
       [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
     eta_contract_thm (is_pred pred_arities) |>
-    RuleCases.save thm
+    Rule_Cases.save thm
   end;
 
 val to_pred_att = Thm.rule_attribute o to_pred;
@@ -374,7 +374,7 @@
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (HOL_basic_ss addsimps to_set_simps
         addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
-    RuleCases.save thm
+    Rule_Cases.save thm
   end;
 
 val to_set_att = Thm.rule_attribute o to_set;
@@ -522,7 +522,7 @@
       Inductive.declare_rules kind rec_name coind no_ind cnames
       (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
       (map (fn th => (to_set [] (Context.Proof ctxt3) th,
-         map fst (fst (RuleCases.get th)))) elims)
+         map fst (fst (Rule_Cases.get th)))) elims)
       raw_induct' ctxt3
   in
     ({intrs = intrs', elims = elims', induct = induct,