diff -r a965cad7d455 -r 8df08902da6f src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Wed Sep 27 21:32:15 2006 +0200
+++ b/src/Pure/General/source.ML	Wed Sep 27 21:33:13 2006 +0200
@@ -20,7 +20,6 @@
   val of_string: string -> (string, string list) source
   val exhausted: ('a, 'b) source -> ('a, 'a list) source
   val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
-  val of_instream_slurp: TextIO.instream -> (string, unit) source
   val tty: (string, unit) source
   val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
     ('a * 'b list -> 'c list * ('a * 'b list)) option ->
@@ -134,21 +133,6 @@
 val tty = of_stream TextIO.stdIn TextIO.stdOut;
 
 
-(* no prompt output, slurp input eagerly *)
-(* NB: if canInput isn't supported, falls back to line input *)
-
-fun drain_stream' instream _ () =
-    let fun lines xs =
-          (case TextIO.canInput (instream, 1) of
-              NONE => xs
-              | SOME 0 => ""::xs (* EOF *)
-              | SOME _ => lines ((TextIO.inputLine instream) :: xs))
-           handle Io => xs
-    in (flat (map explode (rev (lines [TextIO.inputLine instream]))), ()) end;
-
-fun of_instream_slurp instream =
-  make_source [] () default_prompt (drain_stream' instream);
-
 
 (** compose sources **)