src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

   in one_line_proof ^ isar_proof end
 
 fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
   (case play of
     Played _ => meth = SMT2_Method andalso smt_proofs <> SOME true
-  | Play_Timed_Out _ => true
-  | Play_Failed => true
-  | Not_Played => false)
+  | Play_Timed_Out time => Time.> (time, Time.zeroTime)
+  | Play_Failed => true)
 
 fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
     (one_line_params as (preplay, _, _, _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then