# HG changeset patch
# User blanchet
# Date 1305637896 -7200
# Node ID be0e66ccebfa826c306b8ff63679cf1636639b15
# Parent  b04436548927c1321d606c3328ecf002df9bd1aa
append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism

diff -r b04436548927 -r be0e66ccebfa src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 16 23:41:10 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 17 15:11:36 2011 +0200
@@ -672,26 +672,32 @@
                       |> map string_for_hyper_pconst));
           relevant [] [] hopeful
         end
-    fun add_facts ths accepts =
-      (facts |> filter (member Thm.eq_thm ths o snd)) @
-      (accepts |> filter_out (member Thm.eq_thm ths o snd))
+    fun prepend_facts ths accepts =
+      ((facts |> filter (member Thm.eq_thm ths o snd)) @
+       (accepts |> filter_out (member Thm.eq_thm ths o snd)))
       |> take max_relevant
+    fun append_facts ths accepts =
+      let val add = facts |> filter (member Thm.eq_thm ths o snd) in
+        (accepts |> filter_out (member Thm.eq_thm ths o snd)
+                 |> take (max_relevant - length add)) @
+        add
+      end
     fun uses_const s t =
       fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
                   false
     fun maybe_add_set_const (s, ths) accepts =
       accepts |> (if exists (uses_const s o prop_of o snd) accepts orelse
                      exists (uses_const s) (concl_t :: hyp_ts) then
-                    add_facts ths
+                    append_facts ths
                   else
                     I)
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
           |> iter 0 max_relevant threshold0 goal_const_tab []
-          |> not (null add_ths) ? add_facts add_ths
+          |> not (null add_ths) ? prepend_facts add_ths
           |> (fn accepts =>
                  accepts |> could_benefit_from_ext is_built_in_const accepts
-                            ? add_facts @{thms ext}
+                            ? append_facts @{thms ext}
                          |> fold maybe_add_set_const set_consts)
           |> tap (fn accepts => trace_msg ctxt (fn () =>
                       "Total relevant: " ^ string_of_int (length accepts)))