diff -r 18b41bba42b5 -r 1adaefa63c5a src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jan 28 11:48:49 2010 +0100
+++ b/src/HOL/HOL.thy	Sun Jan 31 15:22:40 2010 +0100
@@ -1453,6 +1453,7 @@
   val atomize = @{thms induct_atomize}
   val rulify = @{thms induct_rulify'}
   val rulify_fallback = @{thms induct_rulify_fallback}
+  val equal_def = @{thm induct_equal_def}
   fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
     | dest_def _ = NONE
   val trivial_tac = match_tac @{thms induct_trueI}