1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 00:37:42 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 00:37:42 2011 +0200
     1.3 @@ -940,12 +940,11 @@
     1.4  
     1.5  fun do_introduce_combinators ctxt Ts t =
     1.6    let val thy = Proof_Context.theory_of ctxt in
     1.7 -    t |> not (Meson.is_fol_term thy t)
     1.8 -         ? (conceal_bounds Ts
     1.9 -            #> cterm_of thy
    1.10 -            #> Meson_Clausify.introduce_combinators_in_cterm
    1.11 -            #> prop_of #> Logic.dest_equals #> snd
    1.12 -            #> reveal_bounds Ts)
    1.13 +    t |> conceal_bounds Ts
    1.14 +      |> cterm_of thy
    1.15 +      |> Meson_Clausify.introduce_combinators_in_cterm
    1.16 +      |> prop_of |> Logic.dest_equals |> snd
    1.17 +      |> reveal_bounds Ts
    1.18    end
    1.19    (* A type variable of sort "{}" will make abstraction fail. *)
    1.20    handle THM _ => t |> do_conceal_lambdas Ts