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