1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML	Mon Nov 09 21:30:54 2009 +0100
     1.3 @@ -0,0 +1,28 @@
     1.4 +(*  Title:      Pure/ML-Systems/polyml-5.2.1.ML
     1.5 +
     1.6 +Compatibility wrapper for Poly/ML 5.2.1.
     1.7 +*)
     1.8 +
     1.9 +use "ML-Systems/unsynchronized.ML";
    1.10 +
    1.11 +open Thread;
    1.12 +
    1.13 +structure ML_Name_Space =
    1.14 +struct
    1.15 +  open PolyML.NameSpace;
    1.16 +  type T = PolyML.NameSpace.nameSpace;
    1.17 +  val global = PolyML.globalNameSpace;
    1.18 +end;
    1.19 +
    1.20 +fun reraise exn = raise exn;
    1.21 +
    1.22 +use "ML-Systems/polyml_common.ML";
    1.23 +use "ML-Systems/multithreading_polyml.ML";
    1.24 +
    1.25 +val pointer_eq = PolyML.pointerEq;
    1.26 +
    1.27 +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    1.28 +
    1.29 +use "ML-Systems/compiler_polyml-5.2.ML";
    1.30 +use "ML-Systems/pp_polyml.ML";
    1.31 +