src/Pure/ML-Systems/polyml-5.1.ML
changeset 32776 1504f9c2d060
parent 31427 5a07cc86675d
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Wed Sep 30 09:25:18 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Wed Sep 30 11:36:12 2009 +0200
@@ -5,6 +5,7 @@
 
 fun reraise exn = raise exn;
 
+use "ML-Systems/unsynchronized.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/polyml_common.ML";