diff -r 6852373aae8a -r aa899bce7c3b src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Wed May 30 23:32:54 2007 +0200
+++ b/src/Pure/General/source.ML	Thu May 31 01:25:24 2007 +0200
@@ -124,7 +124,9 @@
     else
       (TextIO.output (outstream, prompt);
         TextIO.flushOut outstream;
-        (input @ explode (TextIO.inputLine instream), ()))
+        (case TextIO.inputLine instream of
+          SOME line => (input @ explode line, ())
+        | NONE => (input, ())))
   end;
 
 fun of_stream instream outstream =