src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/HOL/HOL.thy	Tue Sep 20 05:47:11 2011 +0200
@@ -26,6 +26,7 @@
   ("Tools/simpdata.ML")
   "~~/src/Tools/atomize_elim.ML"
   "~~/src/Tools/induct.ML"
+  ("~~/src/Tools/induction.ML")
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
   ("Tools/cnf_funcs.ML")
@@ -1490,8 +1491,10 @@
 )
 *}
 
+use "~~/src/Tools/induction.ML"
+
 setup {*
-  Induct.setup #>
+  Induct.setup #> Induction.setup #>
   Context.theory_map (Induct.map_simpset (fn ss => ss
     setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
       map (Simplifier.rewrite_rule (map Thm.symmetric