--- a/src/HOL/Tools/Function/mutual.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Tue Feb 10 14:48:26 2015 +0100
@@ -267,8 +267,8 @@
@{thms HOL.notE[OF Sum_Type.sum.distinct(1)] HOL.notE[OF Sum_Type.sum.distinct(2)]}
fun prep_subgoal i =
- REPEAT (eresolve_tac @{thms Pair_inject Inl_inject[elim_format] Inr_inject[elim_format]} i)
- THEN REPEAT (Tactic.eresolve_tac sum_elims i)
+ REPEAT (eresolve_tac ctxt @{thms Pair_inject Inl_inject[elim_format] Inr_inject[elim_format]} i)
+ THEN REPEAT (eresolve_tac ctxt sum_elims i)
in
cases_rule
|> Thm.forall_elim P