diff -r 95d8a2f2bffe -r 1ace987e22e5 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 00:37:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 00:37:42 2011 +0200
@@ -940,12 +940,11 @@
 
 fun do_introduce_combinators ctxt Ts t =
   let val thy = Proof_Context.theory_of ctxt in
-    t |> not (Meson.is_fol_term thy t)
-         ? (conceal_bounds Ts
-            #> cterm_of thy
-            #> Meson_Clausify.introduce_combinators_in_cterm
-            #> prop_of #> Logic.dest_equals #> snd
-            #> reveal_bounds Ts)
+    t |> conceal_bounds Ts
+      |> cterm_of thy
+      |> Meson_Clausify.introduce_combinators_in_cterm
+      |> prop_of |> Logic.dest_equals |> snd
+      |> reveal_bounds Ts
   end
   (* A type variable of sort "{}" will make abstraction fail. *)
   handle THM _ => t |> do_conceal_lambdas Ts