# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID 944b19ab60037d6c03f7fb16e240824dfee350a4
# Parent  42330f25142c9675f43dd4fed7f60a3a30e6e312
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP

diff -r 42330f25142c -r 944b19ab6003 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 27 10:30:08 2011 +0200
@@ -338,13 +338,13 @@
     (hd ss, map unmangled_type (tl ss))
   end
 
-fun introduce_proxies format type_sys tm =
+fun introduce_proxies format type_sys =
   let
-    fun aux ary top_level (CombApp (tm1, tm2)) =
-        CombApp (aux (ary + 1) top_level tm1, aux 0 false tm2)
-      | aux ary top_level (CombConst (name as (s, _), T, T_args)) =
+    fun intro top_level (CombApp (tm1, tm2)) =
+        CombApp (intro top_level tm1, intro false tm2)
+      | intro top_level (CombConst (name as (s, _), T, T_args)) =
         (case proxify_const s of
-           SOME (proxy_ary, proxy_base) =>
+           SOME (_, proxy_base) =>
            if top_level orelse is_setting_higher_order format type_sys then
              case (top_level, s) of
                (_, "c_False") => (`I tptp_false, [])
@@ -354,20 +354,15 @@
              | (false, "c_disj") => (`I tptp_or, [])
              | (false, "c_implies") => (`I tptp_implies, [])
              | (false, s) =>
-               (* Proxies are not needed in THF, but we generate them for "="
-                  when it is not fully applied to work around parsing bugs in
-                  the provers ("= @ x @ x" is challenging to some). *)
-               if is_tptp_equal s andalso ary = proxy_ary then
-                 (`I tptp_equal, [])
-               else
-                 (proxy_base |>> prefix const_prefix, T_args)
+               if is_tptp_equal s then (`I tptp_equal, [])
+               else (proxy_base |>> prefix const_prefix, T_args)
              | _ => (name, [])
            else
              (proxy_base |>> prefix const_prefix, T_args)
           | NONE => (name, T_args))
         |> (fn (name, T_args) => CombConst (name, T, T_args))
-      | aux _ _ tm = tm
-  in aux 0 true tm end
+      | intro _ tm = tm
+  in intro true end
 
 fun combformula_from_prop thy format type_sys eq_as_iff =
   let