# 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()));