# HG changeset patch
# User blanchet
# Date 1312903997 -7200
# Node ID 3cae913850860371dc4502cd6f2716cb4632d9b3
# Parent  6e943b3d27674fb9476dd911e85c616943373452
workaround THF parser limitation

diff -r 6e943b3d2767 -r 3cae91385086 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 09 17:33:17 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 09 17:33:17 2011 +0200
@@ -871,8 +871,13 @@
              | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
              | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
              | (false, s) =>
-               if is_tptp_equal s then IConst (`I tptp_equal, T, [])
-               else IConst (proxy_base |>> prefix const_prefix, T, T_args)
+               if is_tptp_equal s andalso length args = 2 then
+                 IConst (`I tptp_equal, T, [])
+               else
+                 (* Use a proxy even for partially applied THF equality, because
+                    the LEO-II and Satallax parsers complain about not being
+                    able to infer the type of "=". *)
+                 IConst (proxy_base |>> prefix const_prefix, T, T_args)
              | _ => IConst (name, T, [])
            else
              IConst (proxy_base |>> prefix const_prefix, T, T_args)