# HG changeset patch
# User blanchet
# Date 1311115062 -7200
# Node ID 1ace987e22e576e48c014abe28affe2ac42e38f4
# Parent  95d8a2f2bffe3a8b1b89b8fe09cf95336ae96218
avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"

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