| changeset 61841 | 4d3527b94f2a |
| parent 61799 | 4cf66f21b764 |
| child 63432 | ba7901e94e7b |
--- a/src/HOL/Fun_Def.thy Sat Dec 12 15:37:42 2015 +0100 +++ b/src/HOL/Fun_Def.thy Sun Dec 13 21:56:15 2015 +0100 @@ -103,7 +103,7 @@ ML_file "Tools/Function/induction_schema.ML" method_setup induction_schema = \<open> - Scan.succeed (EMPTY_CASES oo Induction_Schema.induction_schema_tac) + Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac) \<close> "prove an induction principle"