src/Pure/ML-Systems/polyml-4.1.4-patch.ML
author wenzelm
Fri, 06 Jan 2006 18:18:16 +0100
changeset 18598 94d658871c98
parent 18160 fb93c63c62f1
child 21299 4b01726d71fc
permissions -rw-r--r--
prep_meta_eq: reuse mk_rews of local simpset; adapted ML code to common conventions; tuned;

(*  Title:      Pure/ML-Systems/polyml-4.1.4-patch.ML
    ID:         $Id$
    Author:     Makarius

Turn the official PolyML 4.2.0 into the internal version 4.1.4, in
order to make it work with Isabelle2005.  This is to be commited 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;

structure Substring =
struct
  open Substring;
  val all = full;
end;