tuning
authorblanchet
Tue, 01 Feb 2022 09:21:50 +0100
changeset 75046 52b37e8a617b
parent 75045 f47410c603c6
child 75047 7d2a5d1f09af
tuning
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