src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

       preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
         (!preplay_data)
     end
   | set_preplay_outcomes_of_isar_step _ _ _ _ _ _ = ()
 
-fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Not_Played
+fun peek_at_outcome outcome =
+  if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
 
 fun get_best_method_outcome force =
   tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *)
   #> map (apsnd force)
   #> sort (play_outcome_ord o pairself snd)

     if forall (not o Lazy.is_finished o snd) meths_outcomes then
       (case Lazy.force outcome1 of
         outcome as Played _ => outcome
       | _ => snd (get_best_method_outcome Lazy.force meths_outcomes))
     else
-      (case get_best_method_outcome peek_at_outcome meths_outcomes of
-        (_, Not_Played) => snd (get_best_method_outcome Lazy.force meths_outcomes)
-      | (_, outcome) => outcome)
+      let val outcome = snd (get_best_method_outcome peek_at_outcome meths_outcomes) in
+        if outcome = Play_Timed_Out Time.zeroTime then
+          snd (get_best_method_outcome Lazy.force meths_outcomes)
+        else
+          outcome
+      end
   end
 
 fun preplay_outcome_of_isar_step_for_method preplay_data l =
   AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
-  #> the_default (Lazy.value Not_Played)
+  #> the_default (Lazy.value (Play_Timed_Out Time.zeroTime))
 
 fun fastest_method_of_isar_step preplay_data =
   the o Canonical_Label_Tab.lookup preplay_data
   #> get_best_method_outcome Lazy.force
   #> fst