changeset 59507 | b468e0f8da2a |
parent 59504 | 8c6747dba731 |
parent 59498 | 50b60f501b05 |
child 59512 | 9bf568cc71a4 |
--- a/src/HOL/Fun.thy Tue Feb 10 17:37:06 2015 +0000 +++ b/src/HOL/Fun.thy Wed Feb 11 12:01:56 2015 +0000 @@ -851,8 +851,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