src/Pure/ML-Systems/alice.ML
changeset 23139 aa899bce7c3b
parent 22837 82cceaf768c8
child 23826 463903573934
     1.1 --- a/src/Pure/ML-Systems/alice.ML	Wed May 30 23:32:54 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/alice.ML	Thu May 31 01:25:24 2007 +0200
     1.3 @@ -104,11 +104,7 @@
     1.4  structure TextIO =
     1.5  struct
     1.6    open TextIO;
     1.7 -
     1.8 -  fun inputLine is =
     1.9 -    (case TextIO.inputLine is of
    1.10 -      SOME str => str
    1.11 -    | NONE => "")
    1.12 +  fun inputLine is = TextIO.inputLine is
    1.13      handle IO.Io _ => raise Interrupt;
    1.14  end;
    1.15