# HG changeset patch
# User blanchet
# Date 1643703710 -3600
# Node ID 52b37e8a617b97e4208e9d58ea9f13825dc97b89
# Parent  f47410c603c61a38fcd2ec7bbd0e0410fc37515e
tuning

diff -r f47410c603c6 -r 52b37e8a617b src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 01 08:59:35 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 01 09:21:50 2022 +0100
@@ -71,12 +71,12 @@
 
 fun max_outcome outcomes =
   let
-    val result = find_first (fn (SH_Some _, _) => true | _ => false) outcomes
+    val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes
     val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes
     val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes
     val none = find_first (fn (SH_None, _) => true | _ => false) outcomes
   in
-    result
+    some
     |> alternative snd unknown
     |> alternative snd timeout
     |> alternative snd none