# HG changeset patch
# User wenzelm
# Date 911998746 -3600
# Node ID 9c0c69ab7d02a9fe887d6aeaa76c415aaf78f0d4
# Parent  ab4d13e9e77a16109516d922318710c3b707e51a
tuned space;

diff -r ab4d13e9e77a -r 9c0c69ab7d02 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Wed Nov 25 13:57:44 1998 +0100
+++ b/src/Pure/tctical.ML	Wed Nov 25 13:59:06 1998 +0100
@@ -198,7 +198,7 @@
 
 (*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));
 
@@ -232,7 +232,7 @@
 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;