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 =  
-  (writeln "** Press RETURN to continue: ";
+  (writeln "** Press RETURN to continue:";
    if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
    else (writeln "Goodbye";  Seq.empty));
 
 exception TRACE_EXIT of thm
 and TRACE_QUIT;

 
 (*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;
-                 writeln "** 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 =