1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     1.3 @@ -885,11 +885,18 @@
     1.4    subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
     1.5                      (0 upto length Ts - 1 ~~ Ts))
     1.6  
     1.7 +fun is_fun_equality (@{const_name HOL.eq},
     1.8 +                     Type (_, [Type (@{type_name fun}, _), _])) = true
     1.9 +  | is_fun_equality _ = false
    1.10 +
    1.11  fun extensionalize_term ctxt t =
    1.12 -  let val thy = Proof_Context.theory_of ctxt in
    1.13 -    t |> cterm_of thy |> Meson.extensionalize_conv ctxt
    1.14 -      |> prop_of |> Logic.dest_equals |> snd
    1.15 -  end
    1.16 +  if exists_Const is_fun_equality t then
    1.17 +    let val thy = Proof_Context.theory_of ctxt in
    1.18 +      t |> cterm_of thy |> Meson.extensionalize_conv ctxt
    1.19 +        |> prop_of |> Logic.dest_equals |> snd
    1.20 +    end
    1.21 +  else
    1.22 +    t
    1.23  
    1.24  fun introduce_combinators_in_term ctxt kind t =
    1.25    let val thy = Proof_Context.theory_of ctxt in