# HG changeset patch
# User blanchet
# Date 1378917467 -7200
# Node ID f7e987ef730405404199d4ba286d4b9c3dec9e61
# Parent  2176a7e407863753c3121f0717366649b492702c
reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently

diff -r 2176a7e40786 -r f7e987ef7304 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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