changeset 59498 | 50b60f501b05 |
parent 58889 | 5b7a9633cfa8 |
child 59507 | b468e0f8da2a |
--- a/src/HOL/Fun.thy Tue Feb 10 14:29:36 2015 +0100 +++ b/src/HOL/Fun.thy Tue Feb 10 14:48:26 2015 +0100 @@ -839,8 +839,8 @@ | (T, SOME rhs) => SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs)) (fn _ => - resolve_tac [eq_reflection] 1 THEN - resolve_tac @{thms ext} 1 THEN + resolve_tac ctxt [eq_reflection] 1 THEN + resolve_tac ctxt @{thms ext} 1 THEN simp_tac (put_simpset ss ctxt) 1)) end in proc end