# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID d64956b03c70a7ca35086031d6cfbd57ab2cd84c
# Parent  f5229ab54284933d87df88a64138ad4ee77b1586
consider "finite" overloaded in "precise_overloaded_args" mode

diff -r f5229ab54284 -r d64956b03c70 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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)