# HG changeset patch
# User blanchet
# Date 1282155423 -7200
# Node ID bbb0982656eb6d48e244045600565a201e6c3fea
# Parent  af205f4fd0f3cfa0f299698cc64995c00ca55543
make sure that "add:" doesn't influence the relevance filter too much

diff -r af205f4fd0f3 -r bbb0982656eb src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 18 19:57:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Aug 18 20:17:03 2010 +0200
@@ -561,13 +561,14 @@
       checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
           (map (name_thms_pair_from_ref ctxt chained_ths) add @
            (if only then [] else all_name_thms_pairs ctxt chained_ths))
+      |> make_unique
       |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse
                                not (is_dangerous_term full_types (prop_of th)))
   in
     relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant relevance_override
                      axioms (concl_t :: hyp_ts)
-    |> make_unique |> sort_wrt fst
+    |> sort_wrt fst
   end
 
 end;