consider "finite" overloaded in "precise_overloaded_args" mode

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -74,6 +74,7 @@
    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
    length (Defs.specifications_of (Theory.defs_of thy) s) > 1)