diff -r 141d8f575f6f -r beb95bf66b21 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 17 11:55:40 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 17 11:56:34 2013 +0100
@@ -741,7 +741,7 @@
         and do_case outer (c, infs) =
           Assume (label_of_clause c, prop_of_clause c) ::
           map (isar_step_of_direct_inf outer) infs
-        val (isar_proof, (preplay_fail, ext_time)) =
+        val (isar_proof, (preplay_fail, preplay_time)) =
           ref_graph
           |> redirect_graph axioms tainted
           |> map (isar_step_of_direct_inf true)
@@ -771,8 +771,8 @@
           let
             val msg =
               (if preplay then
-                [if preplay_fail then "may fail"
-                 else string_from_ext_time ext_time]
+                [(if preplay_fail then "may fail, " else "") ^
+                   Sledgehammer_Preplay.string_of_preplay_time preplay_time]
                else
                  []) @
               (if verbose then