# HG changeset patch
# User paulson
# Date 875182207 -7200
# Node ID 40856b593501652943d11c6498426b0e4e1bada1
# Parent  e57b5902822f9bbf41576e21656af60239e0c8b4
Prints warnings using the "warning" function instead of "writeln"

diff -r e57b5902822f -r 40856b593501 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Sep 25 12:09:41 1997 +0200
+++ b/src/Pure/goals.ML	Thu Sep 25 12:10:07 1997 +0200
@@ -329,7 +329,7 @@
      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)));
@@ -351,9 +351,9 @@
 	  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()));