tuned warning;

--- 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);