diff -r f6927a08a02b -r 1f6b6a7314cf src/Pure/ML-Systems/polyml-old-basis.ML
--- a/src/Pure/ML-Systems/polyml-old-basis.ML	Thu May 31 01:25:35 2007 +0200
+++ b/src/Pure/ML-Systems/polyml-old-basis.ML	Thu May 31 01:36:08 2007 +0200
@@ -6,10 +6,10 @@
 
 structure String =
 struct
-  open String;
   fun isSuffix s1 s2 =
     let val n1 = size s1 and n2 = size s2
     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
+  open String;
 end;
 
 structure Substring =
@@ -28,3 +28,11 @@
     val mkTextWriter = mkWriter;
   end;
 end;
+
+structure TextIO =
+struct
+  open TextIO;
+  fun inputLine is =
+    let val s = TextIO.inputLine is
+    in if s = "" then NONE else SOME s end;
+end;