src/Pure/goals.ML

 fun by_com tac ((th,ths), pairs) : gstack =
   (case  Sequence.pull(tac th)  of
      None      => error"by: tactic failed"
    | Some(th2,ths2) => 
        (if eq_thm(th,th2) 
-	  then writeln "Warning: same as previous level"
+	  then warning "Warning: same as previous level"
 	  else if eq_thm_sg(th,th2) then ()
 	  else writeln ("Warning: signature of proof state has changed" ^
 		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
        ((th2,ths2)::(th,ths)::pairs)));
 

   | backtrack ((th,thstr) :: pairs) =
      (case Sequence.pull thstr of
 	  None      => (writeln"Going back a level..."; backtrack pairs)
 	| Some(th2,thstr2) =>  
 	   (if eq_thm(th,th2) 
-	      then writeln "Warning: same as previous choice at this level"
+	      then warning "Warning: same as previous choice at this level"
 	      else if eq_thm_sg(th,th2) then ()
-	      else writeln "Warning: signature of proof state has changed";
+	      else warning "Warning: signature of proof state has changed";
 	    (th2,thstr2)::pairs));
 
 fun back() = setstate (backtrack (getstate()));
 
 (*Chop back to previous level of the proof*)