src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

           : prover_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 (rev xs) ([], result) end
+  in min timeout xs ([], result) end
 
 fun binary_minimize test timeout result xs =
   let
     fun min depth (result as {run_time, ...} : prover_result) sup
             (xs as _ :: _ :: _) =

     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
-    (* 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"). *)
+    (* Push chained facts to the back, so that they are less likely to be
+       kicked out by the linear minimization algorithm. *)
     val facts = non_chained @ chained
   in
     (print silent (fn () => "Sledgehammer minimizer: " ^
                             quote prover_name ^ ".");
      case test timeout facts of