reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 18:32:43 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 18:37:47 2013 +0200
@@ -239,7 +239,8 @@
       | is_interesting_subterm (Free _) = true
       | is_interesting_subterm _ = false
     fun interest_of_bool t =
-      if exists_Const (is_technical_const orf is_low_level_class_const) t then
+      if exists_Const (is_technical_const orf is_low_level_class_const orf
+                       type_has_top_sort o snd) t then
         Deal_Breaker
       else if exists_type (exists_subtype (curry (op =) @{typ prop})) t orelse
               not (exists_subterm is_interesting_subterm t) then