--- a/src/Pure/ML-Systems/polyml-5.2.1.ML Thu May 24 15:11:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-5.2.1.ML
-
-Compatibility wrapper for Poly/ML 5.2.1.
-*)
-
-open Thread;
-
-structure ML_Name_Space =
-struct
- open PolyML.NameSpace;
- type T = PolyML.NameSpace.nameSpace;
- val global = PolyML.globalNameSpace;
-end;
-
-fun reraise exn = raise exn;
-fun set_exn_serial (_: int) (exn: exn) = exn;
-fun get_exn_serial (exn: exn) : int option = NONE;
-
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/multithreading_polyml.ML";
-use "ML-Systems/unsynchronized.ML";
-
-val _ = PolyML.Compiler.forgetValue "ref";
-val _ = PolyML.Compiler.forgetType "ref";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-use "ML-Systems/compiler_polyml-5.2.ML";
-use "ML-Systems/pp_polyml.ML";
-use "ML-Systems/pp_dummy.ML";
-
-use "ML-Systems/ml_system.ML";
-