# HG changeset patch
# User wenzelm
# Date 911998664 -3600
# Node ID ab4d13e9e77a16109516d922318710c3b707e51a
# Parent  6727d29d164f20c1ea37e8d4e5c2653a6bceda81
replaced prs by writeln;

diff -r 6727d29d164f -r ab4d13e9e77a src/Pure/search.ML
--- a/src/Pure/search.ML	Wed Nov 25 13:57:17 1998 +0100
+++ b/src/Pure/search.ML	Wed Nov 25 13:57:44 1998 +0100
@@ -225,12 +225,12 @@
 	 (case  partition satpred prfs  of
 	      ([],[]) => []
 	    | ([],nonsats) => 
-		  (message("breadth=" ^ string_of_int(length nonsats) ^ "\n");
+		  (message("breadth=" ^ string_of_int(length nonsats));
 		   bfs (List.concat (map tacf nonsats)))
 	    | (sats,_)  => sats)
   in (fn st => Seq.of_list (bfs [st])) end;
 
-val BREADTH_FIRST = gen_BREADTH_FIRST prs;
+val BREADTH_FIRST = gen_BREADTH_FIRST writeln;
 val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
 
 
diff -r 6727d29d164f -r ab4d13e9e77a src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Nov 25 13:57:17 1998 +0100
+++ b/src/Pure/tactic.ML	Wed Nov 25 13:57:44 1998 +0100
@@ -102,7 +102,7 @@
 fun trace_goalno_tac tac i st =  
     case Seq.pull(tac i st) of
 	None    => Seq.empty
-      | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
+      | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected"); 
     			 Seq.make(fn()=> seqcell));
 
 
diff -r 6727d29d164f -r ab4d13e9e77a src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Wed Nov 25 13:57:17 1998 +0100
+++ b/src/Pure/tctical.ML	Wed Nov 25 13:57:44 1998 +0100
@@ -198,9 +198,9 @@
 
 (*Pause until a line is typed -- if non-empty then fail. *)
 fun pause_tac st =  
-  (prs"** Press RETURN to continue: ";
+  (writeln "** Press RETURN to continue: ";
    if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
-   else (prs"Goodbye\n";  Seq.empty));
+   else (writeln "Goodbye";  Seq.empty));
 
 exception TRACE_EXIT of thm
 and TRACE_QUIT;
@@ -216,9 +216,9 @@
      | "f\n" => Seq.empty
      | "o\n" => (flag:=false;  tac st)
      | "s\n" => (suppress_tracing:=true;  tac st)
-     | "x\n" => (prs"Exiting now\n";  raise (TRACE_EXIT st))
+     | "x\n" => (writeln "Exiting now";  raise (TRACE_EXIT st))
      | "quit\n" => raise TRACE_QUIT
-     | _     => (prs
+     | _     => (writeln
 "Type RETURN to continue or...\n\
 \     f    - to fail here\n\
 \     o    - to switch tracing off\n\
@@ -232,7 +232,7 @@
 fun tracify flag tac st =
   if !flag andalso not (!suppress_tracing)
            then (print_goals (!goals_limit) st;
-                 prs"** Press RETURN to continue: ";
+                 writeln "** Press RETURN to continue: ";
                  exec_trace_command flag (tac,st))
   else tac st;