# HG changeset patch
# User wenzelm
# Date 869226881 -7200
# Node ID b976967a92fcf21c137cbd0a889604d0e328c45e
# Parent  de271ba8086e57df6644d1ce9c0cc2d2b1e9bd7f
tuned warning;

diff -r de271ba8086e -r b976967a92fc src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri Jul 18 13:52:35 1997 +0200
+++ b/src/Provers/blast.ML	Fri Jul 18 13:54:41 1997 +0200
@@ -480,8 +480,8 @@
 	  
   in Option.SOME (trl, tac) end
   handle Bind => (*reject: conclusion is not just a variable*)
-   (if !trace then (writeln"Warning: ignoring ill-formed elimination rule";
-		    print_thm rl)
+   (if !trace then (warning ("ignoring ill-formed elimination rule\n" ^
+		    string_of_thm rl))
     else ();
     Option.NONE);