1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 09 17:33:17 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 09 17:33:17 2011 +0200
     1.3 @@ -871,8 +871,13 @@
     1.4               | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
     1.5               | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
     1.6               | (false, s) =>
     1.7 -               if is_tptp_equal s then IConst (`I tptp_equal, T, [])
     1.8 -               else IConst (proxy_base |>> prefix const_prefix, T, T_args)
     1.9 +               if is_tptp_equal s andalso length args = 2 then
    1.10 +                 IConst (`I tptp_equal, T, [])
    1.11 +               else
    1.12 +                 (* Use a proxy even for partially applied THF equality, because
    1.13 +                    the LEO-II and Satallax parsers complain about not being
    1.14 +                    able to infer the type of "=". *)
    1.15 +                 IConst (proxy_base |>> prefix const_prefix, T, T_args)
    1.16               | _ => IConst (name, T, [])
    1.17             else
    1.18               IConst (proxy_base |>> prefix const_prefix, T, T_args)