src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

           |> postprocess_remove_unreferenced_steps I
           |> relabel_proof_canonically
           |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
                preplay_timeout)
 
-        val ((preplay_time, preplay_fail), isar_proof) =
+        val (preplay_result, isar_proof) =
           isar_proof
           |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0)
                preplay_interface
           |> isar_try0 ? try0 preplay_timeout preplay_interface
           |> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface)

                   val num_steps = add_proof_steps (steps_of_proof isar_proof) 0
                 in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
                else
                  []) @
               (if do_preplay then
-                [(if preplay_fail then "may fail, " else "") ^ string_of_ext_time preplay_time]
+                [(case preplay_result of
+                   Preplay_Success ext_time => string_of_ext_time ext_time
+                 | Preplay_Failure => "may fail")]
                else
                  [])
           in
             "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
             Active.sendback_markup [Markup.padding_command] isar_text