1.1 --- a/src/ZF/Tools/inductive_package.ML	Thu Oct 04 14:42:11 2007 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Oct 04 14:42:47 2007 +0200
     1.3 @@ -506,7 +506,7 @@
     1.4       val ([induct', mutual_induct'], thy') =
     1.5         thy
     1.6         |> PureThy.add_thms [((co_prefix ^ "induct", induct),
     1.7 -             [case_names, InductAttrib.induct_set big_rec_name]),
     1.8 +             [case_names, Induct.induct_set big_rec_name]),
     1.9             (("mutual_induct", mutual_induct), [case_names])];
    1.10      in ((thy', induct'), mutual_induct')
    1.11      end;  (*of induction_rules*)
    1.12 @@ -528,7 +528,7 @@
    1.13      |> PureThy.add_thms
    1.14        [(("bnd_mono", bnd_mono), []),
    1.15         (("dom_subset", dom_subset), []),
    1.16 -       (("cases", elim), [case_names, InductAttrib.cases_set big_rec_name])]
    1.17 +       (("cases", elim), [case_names, Induct.cases_set big_rec_name])]
    1.18      ||>> (PureThy.add_thmss o map Thm.no_attributes)
    1.19          [("defs", defs),
    1.20           ("intros", intrs)];