author | paulson |
Mon, 15 Mar 2004 10:45:31 +0100 | |
changeset 14466 | b737e523fc6c |
parent 14465 | 8cc21ed7ef41 |
child 14467 | bbfa6b01a55f |
--- 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;