src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

     fun min _ [] p = p
       | min timeout (x :: xs) (seen, result) =
         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
     fun min depth (result as {run_time, ...} : prover_result) sup
             (xs as _ :: _ :: _) =

           val depth = depth + 1
           val timeout = new_timeout timeout run_time
         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
 (*
         |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
 *)

          result as {outcome = NONE, ...} => ([], result)
        | _ => ([x], result))
     | 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
     val ctxt = Proof.context_of state
     val prover =
       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: " ^
                             quote prover_name ^ ".");
      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
            else
              linear_minimize

       val (used_facts, (preplay, message, _)) =
         if minimize then
           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
           (SOME used_facts, (preplay, message, ""))
     in