author | wenzelm |
Mon, 27 Feb 2012 19:53:34 +0100 | |
changeset 46715 | 6236ca7b32a7 |
parent 46714 | a7ca72710dfe |
child 46716 | c45a4427db39 |
--- 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))