src/Pure/ML-Systems/polyml-5.2.ML
changeset 39616 8052101883c3
parent 38635 f76ad0771f67
--- a/src/Pure/ML-Systems/polyml-5.2.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/polyml-5.2.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -3,8 +3,6 @@
 Compatibility wrapper for Poly/ML 5.2.
 *)
 
-use "ML-Systems/unsynchronized.ML";
-
 open Thread;
 
 structure ML_Name_Space =
@@ -17,9 +15,12 @@
 fun reraise exn = raise exn;
 
 use "ML-Systems/polyml_common.ML";
-
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
+use "ML-Systems/unsynchronized.ML";
+
+val _ = PolyML.Compiler.forgetValue "ref";
+val _ = PolyML.Compiler.forgetType "ref";
 
 val pointer_eq = PolyML.pointerEq;