src/Pure/tctical.ML

     (fn st => 
      (print_goals (!goals_limit) st; Seq.single st));
 
 (*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;
 
 (*Tracing flags*)

    case TextIO.inputLine(TextIO.stdIn) of
        "\n" => tac st
      | "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\
 \     s    - to suppress tracing until next entry to a tactical\n\
 \     x    - to exit at this point\n\

 
 (*Extract from a tactic, a thm->thm seq function that handles tracing*)
 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;
 
 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
 fun traced_tac seqf st =