src/HOL/Fun.thy
changeset 55990 41c6b99c5fb7
parent 55467 a5c9002bc54d
child 56015 57e2cfba9c6e
     1.1 --- a/src/HOL/Fun.thy	Fri Mar 07 22:19:52 2014 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Mar 07 22:30:58 2014 +0100
     1.3 @@ -895,7 +895,7 @@
     1.4            SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
     1.5              (fn _ =>
     1.6                rtac eq_reflection 1 THEN
     1.7 -              rtac ext 1 THEN
     1.8 +              rtac @{thm ext} 1 THEN
     1.9                simp_tac (put_simpset ss ctxt) 1))
    1.10      end
    1.11  in proc end