1.1 --- a/src/HOL/Fun.thy	Mon Jun 23 20:00:58 2008 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Jun 23 23:45:39 2008 +0200
     1.3 @@ -509,7 +509,7 @@
     1.4        case find_double t of
     1.5          (T, NONE) => NONE
     1.6        | (T, SOME rhs) =>
     1.7 -          SOME (Goal.prove ctxt [] [] (Term.equals T $ t $ rhs)
     1.8 +          SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
     1.9              (fn _ =>
    1.10                rtac eq_reflection 1 THEN
    1.11                rtac ext 1 THEN