1.1 --- a/src/HOL/HOL.thy	Thu Oct 04 14:42:11 2007 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Oct 04 14:42:47 2007 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    "~~/src/Tools/IsaPlanner/rw_tools.ML"
     1.5    "~~/src/Tools/IsaPlanner/rw_inst.ML"
     1.6    "~~/src/Provers/project_rule.ML"
     1.7 -  "~~/src/Provers/induct_method.ML"
     1.8    "~~/src/Provers/hypsubst.ML"
     1.9    "~~/src/Provers/splitter.ML"
    1.10    "~~/src/Provers/classical.ML"
    1.11 @@ -29,6 +28,7 @@
    1.12    "~~/src/Tools/code/code_target.ML"
    1.13    "~~/src/Tools/code/code_package.ML"
    1.14    "~~/src/Tools/nbe.ML"
    1.15 +  "~~/src/Tools/induct.ML"
    1.16  begin
    1.17  
    1.18  subsection {* Primitive logic *}
    1.19 @@ -1545,17 +1545,16 @@
    1.20  text {* Method setup. *}
    1.21  
    1.22  ML {*
    1.23 -  structure InductMethod = InductMethodFun
    1.24 -  (struct
    1.25 +  structure Induct = InductFun
    1.26 +  (
    1.27      val cases_default = @{thm case_split}
    1.28      val atomize = @{thms induct_atomize}
    1.29      val rulify = @{thms induct_rulify}
    1.30      val rulify_fallback = @{thms induct_rulify_fallback}
    1.31 -  end);
    1.32 +  );
    1.33  *}
    1.34  
    1.35 -setup InductMethod.setup
    1.36 -
    1.37 +setup Induct.setup
    1.38  
    1.39  
    1.40  subsection {* Other simple lemmas and lemma duplicates *}
    1.41 @@ -1711,7 +1710,7 @@
    1.42  val all_conj_distrib = thm "all_conj_distrib";
    1.43  val all_simps = thms "all_simps";
    1.44  val atomize_not = thm "atomize_not";
    1.45 -val case_split = thm "case_split_thm";
    1.46 +val case_split = thm "case_split";
    1.47  val case_split_thm = thm "case_split_thm"
    1.48  val cases_simp = thm "cases_simp";
    1.49  val choice_eq = thm "choice_eq"