more up-to-date error msg
authorpaulson
Mon, 15 Mar 2004 10:45:31 +0100
changeset 14466 b737e523fc6c
parent 14465 8cc21ed7ef41
child 14467 bbfa6b01a55f
more up-to-date error msg
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;