src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 41748 657712cc8847
parent 41726 1ef01508bb9b
child 41769 eb2e39555f98
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Feb 10 16:38:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Feb 10 17:17:31 2011 +0100
     1.3 @@ -74,9 +74,9 @@
     1.4     generated; if it returns "false" for an overloaded constant, the ATP gets a
     1.5     license to do unsound reasoning if the type system is "overloaded_args". *)
     1.6  fun is_overloaded thy s =
     1.7 -  not (!precise_overloaded_args) orelse
     1.8 -  s = @{const_name finite} orelse
     1.9 -  (s <> @{const_name HOL.eq} andalso
    1.10 +  not (s = @{const_name HOL.eq}) andalso
    1.11 +  not (s = @{const_name Metis.fequal}) andalso
    1.12 +  (not (!precise_overloaded_args) orelse s = @{const_name finite} orelse
    1.13     length (Defs.specifications_of (Theory.defs_of thy) s) > 1)
    1.14  
    1.15  fun needs_type_args thy type_sys s =