# HG changeset patch
# User blanchet
# Date 1297354651 -3600
# Node ID 657712cc88474d62c4e64164ea673b7e262a100e
# Parent  f58d4d202924bf7f3c720c55a0ba62cca3dd2e32
fix handling of "fequal" in generated ATP problems -- the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)

diff -r f58d4d202924 -r 657712cc8847 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Feb 10 16:38:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Feb 10 17:17:31 2011 +0100
@@ -74,9 +74,9 @@
    generated; if it returns "false" for an overloaded constant, the ATP gets a
    license to do unsound reasoning if the type system is "overloaded_args". *)
 fun is_overloaded thy s =
-  not (!precise_overloaded_args) orelse
-  s = @{const_name finite} orelse
-  (s <> @{const_name HOL.eq} andalso
+  not (s = @{const_name HOL.eq}) andalso
+  not (s = @{const_name Metis.fequal}) andalso
+  (not (!precise_overloaded_args) orelse s = @{const_name finite} orelse
    length (Defs.specifications_of (Theory.defs_of thy) s) > 1)
 
 fun needs_type_args thy type_sys s =