# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID 8d8f72aa5c0b9bc114374a127c3be8fcc376b5d8
# Parent  a6ed27399ba97139ea46fe831d4f8407964e9378
got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)

diff -r a6ed27399ba9 -r 8d8f72aa5c0b src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -237,9 +237,7 @@
       | is_boring_prop _ _ = true
     val t = prop_of th
   in
-    (is_boring_prop [] (prop_of th) andalso
-     not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
-    exists_type type_has_top_sort t orelse
+    (is_boring_prop [] t andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
     exists_Const (is_technical_const orf is_low_level_class_const) t orelse
     is_that_fact th
   end