src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML

         HEADGOAL (tac_of_proof_method ctxt assmsp meth))
       handle ERROR msg => error ("Preplay error: " ^ msg)
 
     val play_outcome = take_time timeout prove ()
   in
-    (if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
-     play_outcome)
+    if Config.get ctxt trace then preplay_trace ctxt assmsp goal play_outcome else ();
+    play_outcome
   end
 
 fun preplay_isar_step_for_method ctxt timeout meth =
   try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed
 

         (_, Not_Played) => snd (get_best_method_outcome Lazy.force meths_outcomes)
       | (_, outcome) => outcome)
   end
 
 fun preplay_outcome_of_isar_step_for_method preplay_data l =
-  the o AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
+  AList.lookup (op =) (the (Canonical_Label_Tab.lookup preplay_data l))
+  #> the_default (Lazy.value Not_Played)
 
 fun fastest_method_of_isar_step preplay_data =
   the o Canonical_Label_Tab.lookup preplay_data
   #> get_best_method_outcome Lazy.force
   #> fst