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;