be less aggressive at kicking out chained facts

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 14 12:54:26 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 14 13:20:59 2012 +0200
@@ -128,10 +128,11 @@
         case test timeout (xs @ seen) of
           result as {outcome = NONE, used_facts, run_time, ...}
           : prover_result =>
-          min (new_timeout timeout run_time) (filter_used_facts used_facts xs)
-              (filter_used_facts used_facts seen, result)
+          min (new_timeout timeout run_time)
+              (filter_used_facts true used_facts xs)
+              (filter_used_facts false used_facts seen, result)
         | _ => min timeout xs (x :: seen, result)
-  in min timeout xs ([], result) end
+  in min timeout (rev xs) ([], result) end
 
 fun binary_minimize test timeout result xs =
   let
@@ -154,20 +155,21 @@
         in
           case test timeout (sup @ l0) of
             result as {outcome = NONE, used_facts, ...} =>
-            min depth result (filter_used_facts used_facts sup)
-                      (filter_used_facts used_facts l0)
+            min depth result (filter_used_facts true used_facts sup)
+                      (filter_used_facts true used_facts l0)
           | _ =>
             case test timeout (sup @ r0) of
               result as {outcome = NONE, used_facts, ...} =>
-              min depth result (filter_used_facts used_facts sup)
-                        (filter_used_facts used_facts r0)
+              min depth result (filter_used_facts true used_facts sup)
+                        (filter_used_facts true used_facts r0)
             | _ =>
               let
                 val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
                 val (sup, r0) =
-                  (sup, r0) |> pairself (filter_used_facts (map fst sup_r0))
+                  (sup, r0)
+                  |> pairself (filter_used_facts true (map fst sup_r0))
                 val (sup_l, (r, result)) = min depth result (sup @ l) r0
-                val sup = sup |> filter_used_facts (map fst sup_l)
+                val sup = sup |> filter_used_facts true (map fst sup_l)
               in (sup, (l @ r, result)) end
         end
 (*
@@ -183,8 +185,6 @@
     | p => p
   end
 
-fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
-
 fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
                    i n state facts =
   let
@@ -193,8 +193,9 @@
       get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
     fun test timeout = test_facts params silent prover timeout i n state
     val (chained, non_chained) = List.partition is_fact_chained facts
-    (* Push chained facts to the back, so that they are less likely to be kicked
-       out by the linear minimization algorithm. *)
+    (* Pull chained facts to the front, so that they are less likely to be
+       kicked out by the minimization algorithms (cf. "rev" in
+       "linear_minimize"). *)
     val facts = non_chained @ chained
   in
     (print silent (fn () => "Sledgehammer minimizer: " ^
@@ -202,7 +203,7 @@
      case test timeout facts of
        result as {outcome = NONE, used_facts, run_time, ...} =>
        let
-         val facts = filter_used_facts used_facts facts
+         val facts = filter_used_facts true used_facts facts
          val min =
            if length facts >= Config.get ctxt binary_min_facts then
              binary_minimize
@@ -307,7 +308,7 @@
           minimize_facts do_learn minimize_name params
                          (mode <> Normal orelse not verbose) subgoal
                          subgoal_count state
-                         (filter_used_facts used_facts
+                         (filter_used_facts true used_facts
                               (map (apsnd single o untranslated_fact) facts))
           |>> Option.map (map fst)
         else

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 12:54:26 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 13:20:59 2012 +0200
@@ -131,7 +131,10 @@
   val kill_provers : unit -> unit
   val running_provers : unit -> unit
   val messages : int option -> unit
-  val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
+  val is_fact_chained : (('a * stature) * 'b) -> bool
+  val filter_used_facts :
+    bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
+    ((''a * stature) * 'b) list
   val get_prover : Proof.context -> mode -> string -> prover
 end;
 
@@ -483,7 +486,11 @@
    #> (fn ctxt => tac_for_reconstructor reconstr ctxt ths))
   |> timed_apply timeout
 
-fun filter_used_facts used = filter (member (op =) used o fst)
+fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
+
+fun filter_used_facts keep_chained used =
+  filter ((member (op =) used o fst) orf
+          (if keep_chained then is_fact_chained else K false))
 
 fun play_one_line_proof mode debug verbose timeout pairs state i preferred
                         reconstrs =
@@ -862,7 +869,8 @@
            fn () =>
               let
                 val used_pairs =
-                  facts |> map untranslated_fact |> filter_used_facts used_facts
+                  facts |> map untranslated_fact
+                        |> filter_used_facts false used_facts
               in
                 play_one_line_proof mode debug verbose preplay_timeout
                     used_pairs state subgoal (hd reconstrs) reconstrs

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Aug 14 12:54:26 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Aug 14 13:20:59 2012 +0200
@@ -87,7 +87,7 @@
     fun print_used_facts used_facts =
       tag_list 1 facts
       |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
-      |> filter_used_facts used_facts
+      |> filter_used_facts false used_facts
       |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
       |> commas
       |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^