# HG changeset patch
# User wenzelm
# Date 1330368814 -3600
# Node ID 6236ca7b32a7a3dc60499426eaddc7f566558fcd
# Parent  a7ca72710dfe6dd8802613d8cbc4265a284b41c5
tuned;

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