src/Provers/blast.ML

   | matchs (t :: ts) (u :: us) = match t u andalso matchs ts us;
 
 
 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))
   else ();
 

                                 Int.toString lim);
                        if !trace then error "************************\n"
                        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
   in prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end
   handle PROVE     => Seq.empty