src/Pure/General/source.ML
changeset 23661 b3f05bc680b6
parent 23139 aa899bce7c3b
child 23675 2d618c190466
     1.1 --- a/src/Pure/General/source.ML	Mon Jul 09 11:44:20 2007 +0200
     1.2 +++ b/src/Pure/General/source.ML	Mon Jul 09 11:44:22 2007 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4    let val input = slurp_input instream in
     1.5      if exists (fn c => c = "\n") input then (input, ())
     1.6      else
     1.7 -      (TextIO.output (outstream, prompt);
     1.8 +      (TextIO.output (outstream, Output.output prompt);
     1.9          TextIO.flushOut outstream;
    1.10          (case TextIO.inputLine instream of
    1.11            SOME line => (input @ explode line, ())