# HG changeset patch
# User wenzelm
# Date 1128434708 -7200
# Node ID f84b032417acde9e62c044a71f3cf41e8a1ee55e
# Parent  a92cda068ad88f160d99f39446c4213ee62ee46f
Patch for PolyML 4.1.4 to make it work with Isabelle2005.  We commit this into ML_dbase!

diff -r a92cda068ad8 -r f84b032417ac 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;