# HG changeset patch
# User paulson
# Date 1113296862 -7200
# Node ID 7d91dd712ff8b4c0744435e5baa4e3b6207e473b
# Parent  95deeda57341faef6f8c845c5715cf34c1c2a8d5
fixing an incompatibility with Posix.IO.mkTextReader

diff -r 95deeda57341 -r 7d91dd712ff8 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Apr 11 16:25:53 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Apr 12 11:07:42 2005 +0200
@@ -165,3 +165,17 @@
 
 val profiling: int->unit =
      RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;
+
+structure OriginalPosix = Posix;
+structure OriginalIO = Posix.IO;
+
+structure Posix =
+struct
+  open OriginalPosix
+  structure IO =
+  struct
+  open OriginalIO
+  val mkTextReader = mkReader 
+  val mkTextWriter = mkWriter 
+  end;
+end;