src/Pure/ML-Systems/polyml-4.1.4-patch.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml-4.1.4-patch.ML	Tue Oct 04 16:05:08 2005 +0200
@@ -0,0 +1,24 @@
+(*  Title:      Pure/ML-Systems/polyml-4.1.4-patch.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Patch for PolyML 4.1.4 to make it work with Isabelle2005.  We commit
+this into ML_dbase!
+*)
+
+structure Posix =
+struct
+  open Posix;
+  structure IO =
+  struct
+    open IO;
+    val mkReader = mkTextReader;
+    val mkWriter = mkTextWriter;
+  end;
+end;
+
+structure TextIO =
+struct
+  open TextIO;
+  fun inputLine is = Option.getOpt (TextIO.inputLine is, "");
+end;