# HG changeset patch
# User blanchet
# Date 1289179947 -3600
# Node ID 8b73059e97a1836149b73bf2d6e5e03c5184d534
# Parent  a29b2fee592beb80773af3db69f1e63ea761ee61
better detection of completely irrelevant facts

diff -r a29b2fee592b -r 8b73059e97a1 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sun Nov 07 18:19:04 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Nov 08 02:32:27 2010 +0100
@@ -369,13 +369,16 @@
   | locality_bonus {assum_bonus, ...} Assum = assum_bonus
   | locality_bonus {chained_bonus, ...} Chained = chained_bonus
 
+fun is_odd_const_name s =
+  s = abs_name orelse String.isPrefix skolem_prefix s orelse
+  String.isSuffix theory_const_suffix s
+
 fun fact_weight fudge loc const_tab relevant_consts fact_consts =
   case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
                    ||> filter_out (pconst_hyper_mem swap relevant_consts) of
     ([], _) => 0.0
   | (rel, irrel) =>
-    if forall (forall (String.isSuffix theory_const_suffix o fst))
-              [rel, irrel] then
+    if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
       0.0
     else
       let