--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Aug 14 13:20:59 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Aug 14 14:07:53 2012 +0200
@@ -132,7 +132,7 @@
(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
@@ -193,9 +193,8 @@
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: " ^