# HG changeset patch
# User desharna
# Date 1745567181 -7200
# Node ID 46591222e4fc68e0f81dfe916db9b551014bb35c
# Parent  7ab0fb5d9919f59d49ef0dfe8d40d0b0cfd77b20
preserved facts order in Sledgehammer's linear minimizer

diff -r 7ab0fb5d9919 -r 46591222e4fc src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Apr 24 23:29:57 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Apr 25 09:46:21 2025 +0200
@@ -145,7 +145,7 @@
    of the facts are actually needed. The binary algorithm is much more
    appropriate for provers that cannot return the list of used facts and hence
    returns all facts as used. Since we cannot know in advance how many facts are
-   actually needed, we heuristically set the threshold to 10 facts. *)
+   actually needed, we heuristically set the threshold. *)
 val binary_min_facts =
   Attrib.setup_config_int \<^binding>\<open>sledgehammer_minimize_binary_min_facts\<close> (K 20)
 
@@ -153,11 +153,11 @@
   let
     fun min _ [] p = p
       | min timeout (x :: xs) (seen, result) =
-        (case test timeout (xs @ seen) of
+        (case test timeout (seen @ xs) of
           result as {outcome = NONE, used_facts, run_time, ...} : 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))
+        | _ => min timeout xs (seen @ [x], result))
   in
     min timeout xs ([], result)
   end