src/HOL/Tools/Sledgehammer/sledgehammer.ML

   | alternative _ NONE (y as SOME _) = y
   | alternative _ NONE NONE = NONE
 
 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
     |> the_default (SH_Unknown, "")
   end