--- 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,