reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently
authorblanchet
Wed Sep 11 18:37:47 2013 +0200 (2013-09-11)
changeset 53545f7e987ef7304
parent 53544 2176a7e40786
child 53546 a2d2fa096e31
reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 18:32:43 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Sep 11 18:37:47 2013 +0200
     1.3 @@ -239,7 +239,8 @@
     1.4        | is_interesting_subterm (Free _) = true
     1.5        | is_interesting_subterm _ = false
     1.6      fun interest_of_bool t =
     1.7 -      if exists_Const (is_technical_const orf is_low_level_class_const) t then
     1.8 +      if exists_Const (is_technical_const orf is_low_level_class_const orf
     1.9 +                       type_has_top_sort o snd) t then
    1.10          Deal_Breaker
    1.11        else if exists_type (exists_subtype (curry (op =) @{typ prop})) t orelse
    1.12                not (exists_subterm is_interesting_subterm t) then