# HG changeset patch
# User blanchet
# Date 1292427726 -3600
# Node ID b05014180288f8305c80ade3dbbf25fe758018dd
# Parent  4b2a457b17e89948451bab9e0bf8d32ab9eb22a4
move facts supplied with "add:" to the front, so that they get a better weight (SMT)

diff -r 4b2a457b17e8 -r b05014180288 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 15:13:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 16:42:06 2010 +0100
@@ -539,10 +539,8 @@
           relevant [] [] hopeful
         end
     fun add_facts ths accepts =
-      (facts |> filter ((member Thm.eq_thm ths
-                         andf (not o member (Thm.eq_thm o apsnd snd) accepts))
-                        o snd))
-      @ accepts
+      (facts |> filter (member Thm.eq_thm ths o snd)) @
+      (accepts |> filter_out (member Thm.eq_thm ths o snd))
       |> take max_relevant
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)