got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)

--- 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