src/HOL/Fun_Def.thy

--- a/src/HOL/Fun_Def.thy	Mon Aug 18 15:46:27 2014 +0200
+++ b/src/HOL/Fun_Def.thy	Tue Aug 19 12:05:11 2014 +0200
@@ -103,7 +103,7 @@
 ML_file "Tools/Function/induction_schema.ML"
 
 method_setup induction_schema = {*
-  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
+  Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac)
 *} "prove an induction principle"
 
 setup {*