# HG changeset patch
# User desharna
# Date 1648743158 -7200
# Node ID 6e8ca49593346760fcb2c3fbf68099db54f410f0
# Parent  48736d743e8c98ae8c7aaa21c89325e632cad96c
tuned sledehammer to return best succeeding preplay method

diff -r 48736d743e8c -r 6e8ca4959334 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 30 10:37:38 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 31 18:12:38 2022 +0200
@@ -134,23 +134,11 @@
 
 fun select_one_line_proof used_facts preferred_meth preplay_results =
   (case preplay_results of
-    [] => (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
-  | (best_meth, best_outcome, best_used_facts) :: results' =>
-    let
-      val (prefered_outcome, prefered_used_facts) =
-        (case find_first (fn (meth, _, _) => meth = preferred_meth) preplay_results of
-          NONE => (Play_Timed_Out Time.zeroTime, used_facts)
-        | SOME (_, prefered_outcome, prefered_used_facts) =>
-          (prefered_outcome, prefered_used_facts))
-    in
-      (case (prefered_outcome, best_outcome) of
-        (* If prefered_meth succeeded, use it irrespective of other preplay results *)
-        (Played _, _) => (prefered_used_facts, (preferred_meth, prefered_outcome))
-        (* If prefered_meth did not succeed but best method did, use best method *)
-      | (_, Played _) => (best_used_facts, (best_meth, best_outcome))
-        (* If neither succeeded, use preferred_meth *)
-      | (_, _) => (prefered_used_facts, (preferred_meth, prefered_outcome)))
-    end)
+    (* Select best method if preplay succeeded *)
+    (best_meth, best_outcome as Played _, best_used_facts) :: _ =>
+    (best_used_facts, (best_meth, best_outcome))
+    (* Otherwise select preferred method with dummy timeout *)
+  | _ => (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)))
   |> apfst (filter_out (fn (_, (sc, _)) => sc = Chained))
 
 fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn