diff -r a1a48c69d623 -r 096237fe70f1 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -885,11 +885,18 @@
   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
                     (0 upto length Ts - 1 ~~ Ts))
 
+fun is_fun_equality (@{const_name HOL.eq},
+                     Type (_, [Type (@{type_name fun}, _), _])) = true
+  | is_fun_equality _ = false
+
 fun extensionalize_term ctxt t =
-  let val thy = Proof_Context.theory_of ctxt in
-    t |> cterm_of thy |> Meson.extensionalize_conv ctxt
-      |> prop_of |> Logic.dest_equals |> snd
-  end
+  if exists_Const is_fun_equality t then
+    let val thy = Proof_Context.theory_of ctxt in
+      t |> cterm_of thy |> Meson.extensionalize_conv ctxt
+        |> prop_of |> Logic.dest_equals |> snd
+    end
+  else
+    t
 
 fun introduce_combinators_in_term ctxt kind t =
   let val thy = Proof_Context.theory_of ctxt in