--- a/src/ZF/Tools/inductive_package.ML Fri Oct 05 22:00:13 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Oct 05 22:00:15 2007 +0200
@@ -506,7 +506,7 @@
val ([induct', mutual_induct'], thy') =
thy
|> PureThy.add_thms [((co_prefix ^ "induct", induct),
- [case_names, Induct.induct_set big_rec_name]),
+ [case_names, Induct.induct_pred big_rec_name]),
(("mutual_induct", mutual_induct), [case_names])];
in ((thy', induct'), mutual_induct')
end; (*of induction_rules*)
@@ -528,7 +528,7 @@
|> PureThy.add_thms
[(("bnd_mono", bnd_mono), []),
(("dom_subset", dom_subset), []),
- (("cases", elim), [case_names, Induct.cases_set big_rec_name])]
+ (("cases", elim), [case_names, Induct.cases_pred big_rec_name])]
||>> (PureThy.add_thmss o map Thm.no_attributes)
[("defs", defs),
("intros", intrs)];