# HG changeset patch
# User wenzelm
# Date 971983427 -7200
# Node ID b223a9a3350e53a88a391b4872ef1acad6daa92e
# Parent  ea1bf4b6255cb3369ec947614ea945576d813a74
InductAttrib;

diff -r ea1bf4b6255c -r b223a9a3350e src/HOL/Tools/datatype_package.ML
--- 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;
 
 
diff -r ea1bf4b6255c -r b223a9a3350e src/HOL/Tools/inductive_package.ML
--- 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;