got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)
authorblanchet
Tue Sep 10 15:56:51 2013 +0200 (2013-09-10 ago)
changeset 535088d8f72aa5c0b
parent 53507 a6ed27399ba9
child 53509 cf7679195169
got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.3 @@ -237,9 +237,7 @@
     1.4        | is_boring_prop _ _ = true
     1.5      val t = prop_of th
     1.6    in
     1.7 -    (is_boring_prop [] (prop_of th) andalso
     1.8 -     not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
     1.9 -    exists_type type_has_top_sort t orelse
    1.10 +    (is_boring_prop [] t andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
    1.11      exists_Const (is_technical_const orf is_low_level_class_const) t orelse
    1.12      is_that_fact th
    1.13    end