src/Provers/blast.ML

 	  TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i
 	  THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
 	  
   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);
 
 
 (*** Conversion of Introduction Rules ***)