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"
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