diff -r 0a6c24f549c3 -r beed2bc052a3 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Dec 23 17:37:54 2005 +0100
+++ b/src/HOL/HOL.thy	Fri Dec 23 18:36:26 2005 +0100
@@ -1299,7 +1299,6 @@
   shows "(A && B) == Trueprop (induct_conj A B)"
   by (unfold atomize_conj induct_conj_def)
 
-lemmas induct_atomize_old = induct_forall_eq induct_implies_eq induct_equal_eq atomize_conj
 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
 lemmas induct_rulify [symmetric, standard] = induct_atomize
 lemmas induct_rulify_fallback =
@@ -1334,7 +1333,6 @@
   structure InductMethod = InductMethodFun
   (struct
     val cases_default = thm "case_split"
-    val atomize_old = thms "induct_atomize_old"
     val atomize = thms "induct_atomize"
     val rulify = thms "induct_rulify"
     val rulify_fallback = thms "induct_rulify_fallback"