InductAttrib;

--- a/src/HOL/Tools/datatype_package.ML	Thu Oct 19 21:23:15 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 19 21:23:47 2000 +0200
@@ -298,8 +298,8 @@
           |> RuleCases.name (RuleCases.get thm);
 
     fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
-      (("", proj index (length descr) induction), [InductMethod.induct_type_global name]) ::
-      (("", exhaustion), [InductMethod.cases_type_global name]) :: ths;
+      (("", proj index (length descr) induction), [InductAttrib.induct_type_global name]) ::
+      (("", exhaustion), [InductAttrib.cases_type_global name]) :: ths;
   in #1 o PureThy.add_thms (foldl add ([], infos)) end;
 
 

--- a/src/HOL/Tools/inductive_package.ML	Thu Oct 19 21:23:15 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 19 21:23:47 2000 +0200
@@ -382,12 +382,12 @@
     fun cases_spec (name, elim) thy =
       thy
       |> Theory.add_path (Sign.base_name name)
-      |> (#1 o PureThy.add_thms [(("cases", elim), [InductMethod.cases_set_global name])])
+      |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
       |> Theory.parent_path;
     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
 
     fun induct_spec (name, th) = (#1 o PureThy.add_thms
-      [(("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name])]);
+      [(("", th), [RuleCases.case_names induct_cases, InductAttrib.induct_set_global name])]);
     val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
   in Library.apply (cases_specs @ induct_specs) end;