src/Pure/tctical.ML

       Seq.single st));
 
 (*Pause until a line is typed -- if non-empty then fail. *)
 fun pause_tac st =
   (tracing "** Press RETURN to continue:";
-   if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st
+   if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
    else (tracing "Goodbye";  Seq.empty));
 
 exception TRACE_EXIT of thm
 and TRACE_QUIT;
 

 val trace_REPEAT= ref false
 and suppress_tracing = ref false;
 
 (*Handle all tracing commands for current state and tactic *)
 fun exec_trace_command flag (tac, st) =
-   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" => (tracing "Exiting now";  raise (TRACE_EXIT st))
-     | "quit\n" => raise TRACE_QUIT
+   case TextIO.inputLine TextIO.stdIn of
+       SOME "\n" => tac st
+     | SOME "f\n" => Seq.empty
+     | SOME "o\n" => (flag:=false;  tac st)
+     | SOME "s\n" => (suppress_tracing:=true;  tac st)
+     | SOME "x\n" => (tracing "Exiting now";  raise (TRACE_EXIT st))
+     | SOME "quit\n" => raise TRACE_QUIT
      | _     => (tracing
 "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\