| changeset 4280 | 278660f52716 |
| parent 4270 | 957c887b89b5 |
| child 4994 | 8b361563d470 |
--- 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)));