author | wenzelm |
Sat, 22 Nov 1997 13:27:02 +0100 | |
changeset 4280 | 278660f52716 |
parent 4279 | 835ea07170a6 |
child 4281 | 6c6073b13600 |
src/Pure/goals.ML | file | annotate | diff | comparison | revisions |
--- 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)));