changeset 58002 | 0ed1e999a0fb |
parent 57959 | 1bfed12a7646 |
child 58305 | 57752a91eec4 |
--- 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 {*