# HG changeset patch
# User wenzelm
# Date 880201622 -3600
# Node ID 278660f52716f923800495ec2eccbe8a93d9f5cb
# Parent  835ea07170a6cba80d5e4533edd3e961baada9dd
fixed warning;

diff -r 835ea07170a6 -r 278660f52716 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Sat Nov 22 13:26:43 1997 +0100
+++ b/src/Pure/goals.ML	Sat Nov 22 13:27:02 1997 +0100
@@ -330,7 +330,7 @@
        (if eq_thm(th,th2) 
 	  then warning "Warning: same as previous 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" ^
 		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
        ((th2,ths2)::(th,ths)::pairs)));