src/Pure/goals.ML
changeset 1580 e3fd931e6095
parent 1565 70dd38777109
child 1628 60136fdd80c4
--- a/src/Pure/goals.ML	Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/goals.ML	Fri Mar 15 12:01:19 1996 +0100
@@ -311,9 +311,9 @@
      None      => error"by: tactic failed"
    | Some(th2,ths2) => 
        (if eq_thm(th,th2) 
-	  then writeln"Warning: same as previous level"
+	  then warning "same as previous level"
 	  else if eq_thm_sg(th,th2) then ()
-	  else writeln("Warning: signature of proof state has changed" ^
+	  else warning("signature of proof state has changed" ^
 		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
        ((th2,ths2)::(th,ths)::pairs)));
 
@@ -333,9 +333,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 "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 "signature of proof state has changed";
 	    (th2,thstr2)::pairs));
 
 fun back() = setstate (backtrack (getstate()));