# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID 0e19032737121e5c5855b6604b316615eb84a834
# Parent  be78f4053bce0c5e965041721ec0a1597c69319d
fix translation of higher-order equality ("fequal") if "precise_overloaded_args" is "true"

diff -r be78f4053bce -r 0e1903273712 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -74,7 +74,8 @@
    license to do unsound reasoning if the type system is "overloaded_args". *)
 fun is_overloaded thy s =
   not (!precise_overloaded_args) orelse
-  length (Defs.specifications_of (Theory.defs_of thy) s) > 1
+  (s <> @{const_name HOL.eq} andalso
+   length (Defs.specifications_of (Theory.defs_of thy) s) > 1)
 
 fun needs_type_args thy type_sys s =
   case type_sys of
@@ -408,8 +409,7 @@
             CombConst (name as (s, s'), _, ty_args) =>
             (case AList.lookup (op =) fname_table s of
                SOME (n, fname) =>
-               if top_level andalso length args = n then (name, [])
-               else (fname, ty_args)
+               (if top_level andalso length args = n then name else fname, [])
              | NONE =>
                case strip_prefix_and_unascii const_prefix s of
                  NONE => (name, ty_args)
@@ -526,7 +526,7 @@
   if explicit_apply then
     NONE
   else
-    SOME (Symtab.empty |> Symtab.update equal_entry |> consider_problem problem)
+    SOME (Symtab.empty |> Symtab.default equal_entry |> consider_problem problem)
 
 fun min_arity_of thy type_sys NONE s =
     (if s = "equal" orelse s = type_tag_name orelse