# HG changeset patch
# User paulson
# Date 1079343931 -3600
# Node ID b737e523fc6c5c1b209043641bea3ef4cdfb0d5c
# Parent  8cc21ed7ef41a9127a55cad9945ee439c957dc88
more up-to-date error msg

diff -r 8cc21ed7ef41 -r b737e523fc6c src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri Mar 12 10:47:59 2004 +0100
+++ b/src/Provers/blast.ML	Mon Mar 15 10:45:31 2004 +0100
@@ -1288,7 +1288,9 @@
 fun blast_tac cs i st = 
     ((DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i 
      THEN flexflex_tac) st
-    handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
+    handle TRANS s =>
+      ((if !trace then warning ("blast: " ^ s) else ()); 
+       Seq.empty);
 
 fun Blast_tac i = blast_tac (Data.claset()) i;