--- a/src/ZF/Tools/inductive_package.ML Thu Oct 04 14:42:11 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Oct 04 14:42:47 2007 +0200
@@ -506,7 +506,7 @@
val ([induct', mutual_induct'], thy') =
thy
|> PureThy.add_thms [((co_prefix ^ "induct", induct),
- [case_names, InductAttrib.induct_set big_rec_name]),
+ [case_names, Induct.induct_set 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, InductAttrib.cases_set big_rec_name])]
+ (("cases", elim), [case_names, Induct.cases_set big_rec_name])]
||>> (PureThy.add_thmss o map Thm.no_attributes)
[("defs", defs),
("intros", intrs)];