--- a/src/HOL/HOL.thy Fri Jul 24 12:32:43 2009 +0200
+++ b/src/HOL/HOL.thy Fri Jul 24 12:33:00 2009 +0200
@@ -1446,7 +1446,7 @@
text {* Method setup. *}
ML {*
-structure Induct = InductFun
+structure Induct = Induct
(
val cases_default = @{thm case_split}
val atomize = @{thms induct_atomize}