fixed warning;
authorwenzelm
Sat, 22 Nov 1997 13:27:02 +0100
changeset 4280 278660f52716
parent 4279 835ea07170a6
child 4281 6c6073b13600
fixed warning;
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)));