| changeset 59953 | 3d207f8f40dd |
| parent 59141 | 9a5c2e9b001e |
| child 60682 | 5a6cd2560549 |
--- a/src/HOL/Fun_Def.thy Wed Apr 08 11:52:35 2015 +0200 +++ b/src/HOL/Fun_Def.thy Wed Apr 08 11:52:53 2015 +0200 @@ -103,7 +103,7 @@ ML_file "Tools/Function/induction_schema.ML" method_setup induction_schema = {* - Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac) + Scan.succeed (EMPTY_CASES oo Induction_Schema.induction_schema_tac) *} "prove an induction principle"