diff -r a7ca72710dfe -r 6236ca7b32a7 src/Provers/blast.ML --- a/src/Provers/blast.ML Mon Feb 27 17:40:59 2012 +0100 +++ b/src/Provers/blast.ML Mon Feb 27 19:53:34 2012 +0100 @@ -1251,7 +1251,7 @@ NONE => (writeln ("PROOF FAILED for depth " ^ string_of_int lim); backtrack trace choices) - | cell => (if (trace orelse stats) + | cell => (if trace orelse stats then writeln (Timing.message (Timing.result start) ^ " for reconstruction") else (); Seq.make(fn()=> cell))