tuned space;
authorwenzelm
Wed, 25 Nov 1998 13:59:06 +0100
changeset 5957 9c0c69ab7d02
parent 5956 ab4d13e9e77a
child 5958 c48efb523a4d
tuned space;
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;