--- 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