# HG changeset patch
# User blanchet
# Date 1282580749 -7200
# Node ID 3a203da3f89b3ec33a6606e0c0086786bd7845bc
# Parent  f9edc593e929d725b37be48e9c56f30b3f5bd21a
weed out junk in relevance filter

diff -r f9edc593e929 -r 3a203da3f89b src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 23 18:04:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 23 18:25:49 2010 +0200
@@ -229,9 +229,7 @@
       case axioms of
         SOME axioms => axioms
       | NONE =>
-        (print_d (fn () => "Selecting relevant facts for " ^ quote atp_name ^
-                           ".");
-         relevant_facts full_types relevance_threshold relevance_convergence
+        (relevant_facts full_types relevance_threshold relevance_convergence
                         defs_relevant
                         (the_default default_max_relevant_per_iter
                                      max_relevant_per_iter)
diff -r f9edc593e929 -r 3a203da3f89b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 18:04:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 18:25:49 2010 +0200
@@ -89,7 +89,8 @@
 val fresh_prefix = "Sledgehammer.FRESH."
 val flip = Option.map not
 (* These are typically simplified away by "Meson.presimplify". *)
-val boring_consts = [@{const_name If}, @{const_name Let}]
+val boring_consts =
+  [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
 
 fun get_consts_typs thy pos ts =
   let
@@ -345,7 +346,7 @@
                    (defs_relevant andalso defines thy th rel_const_tab) then
                   (trace_msg (fn () =>
                        name ^ " passes: " ^ Real.toString weight
-                       (* ^ " consts: " ^ commas (map fst consts_typs) *));
+                       ^ " consts: " ^ commas (map fst consts_typs));
                    relevant ((ax, weight) :: newrels, rejects) axs)
                 else
                   relevant (newrels, ax :: rejects) axs
@@ -386,7 +387,9 @@
 (* FIXME: put other record thms here, or declare as "no_atp" *)
 val multi_base_blacklist =
   ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
-   "split_asm", "cases", "ext_cases", "eq"]
+   "split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy",
+   "case_cong", "weak_case_cong"]
+  |> map (prefix ".")
 
 val max_lambda_nesting = 3
 
@@ -518,7 +521,7 @@
            forall (not o member Thm.eq_thm add_thms) ths0 andalso
            (Facts.is_concealed facts name orelse
             (respect_no_atp andalso is_package_def name) orelse
-            member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
+            exists (fn s => String.isSuffix s name) multi_base_blacklist orelse
             String.isSuffix "_def_raw" (* FIXME: crude hack *) name) then
           I
         else