# HG changeset patch
# User wenzelm
# Date 1223060798 -7200
# Node ID 40c3f900c4572e3159da81624e6ae1bae48128f3
# Parent  404649964f09018ce9c4a0523e1a5cd450832640
removed obsolete Posix/Signal compatibility wrappers;

diff -r 404649964f09 -r 40c3f900c457 src/Pure/ML-Systems/polyml_old_basis.ML
--- a/src/Pure/ML-Systems/polyml_old_basis.ML	Fri Oct 03 21:06:37 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_old_basis.ML	Fri Oct 03 21:06:38 2008 +0200
@@ -21,17 +21,6 @@
   val full = all;
 end;
 
-structure Posix =
-struct
-  open Posix;
-  structure IO =
-  struct
-    open IO;
-    val mkTextReader = mkReader;
-    val mkTextWriter = mkWriter;
-  end;
-end;
-
 structure TextIO =
 struct
   open TextIO;
diff -r 404649964f09 -r 40c3f900c457 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Fri Oct 03 21:06:37 2008 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML	Fri Oct 03 21:06:38 2008 +0200
@@ -193,18 +193,3 @@
   fun fmt a b = Time.fmt (dest_int a) b;
 end;
 
-
-(* Posix *)
-
-structure Posix =
-struct
-  open Posix;
-  structure IO =
-  struct
-    open IO;
-    fun mkTextWriter {appendMode, chunkSize, fd, initBlkMode, name} =
-      IO.mkTextWriter {appendMode = appendMode, chunkSize = dest_int chunkSize,
-        fd = fd, initBlkMode = initBlkMode, name = name};
-  end;
-end;
-