--- a/src/Provers/blast.ML Sun Mar 01 14:45:23 2009 +0100
+++ b/src/Provers/blast.ML Sun Mar 01 16:21:33 2009 +0100
@@ -913,7 +913,7 @@
fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) =
if b then
- writeln (end_timing start ^ " for search. Closed: "
+ writeln (#message (end_timing start) ^ " for search. Closed: "
^ Int.toString (!nclosed) ^
" tried: " ^ Int.toString (!ntried) ^
" tactics: " ^ Int.toString (length tacs))
@@ -1264,7 +1264,7 @@
else ();
backtrack choices)
| cell => (if (!trace orelse !stats)
- then writeln (end_timing start ^ " for reconstruction")
+ then writeln (#message (end_timing start) ^ " for reconstruction")
else ();
Seq.make(fn()=> cell))
end