src/Provers/blast.ML

           in
           case Seq.pull(EVERY' (rev tacs) 1 st) of
               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))
           end
   in