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)

--- 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 =