# HG changeset patch
# User blanchet
# Date 1335521770 -7200
# Node ID 034cc7cc8b4a854e31d270dfa38b9a268a621b18
# Parent  d27bb852c430ae99062ce63a1148b128a3f50979
eta-expand unapplied equalities in THF rather than using a proxy

diff -r d27bb852c430 -r 034cc7cc8b4a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Apr 27 12:16:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Apr 27 12:16:10 2012 +0200
@@ -1076,10 +1076,16 @@
                if is_tptp_equal s andalso length args = 2 then
                  IConst (`I tptp_equal, T, [])
                else
-                 (* Use a proxy even for partially applied THF0 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)
+                 (* Eta-expand partially applied THF equality, because the
+                    LEO-II and Satallax parsers complain about not being able to
+                    infer the type of "=". *)
+                 let val i_T = domain_type T in
+                   IAbs ((`I "X", i_T),
+                         IAbs ((`I "Y", i_T),
+                               IApp (IApp (IConst (`I tptp_equal, T, []),
+                                           IConst (`I "X", i_T, [])),
+                                     IConst (`I "Y", i_T, []))))
+                 end
              | _ => IConst (name, T, [])
            else
              IConst (proxy_base |>> prefix const_prefix, T, T_args)