src/Pure/ML-Systems/polyml.ML
changeset 32294 d00238af17b6
parent 31427 5a07cc86675d
child 32776 1504f9c2d060
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 30 23:37:53 2009 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 30 23:50:11 2009 +0200
@@ -17,7 +17,7 @@
 use "ML-Systems/polyml_common.ML";
 
 if ml_system = "polyml-5.2"
-then use "ML-Systems/thread_dummy.ML"
+then (use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML")
 else use "ML-Systems/multithreading_polyml.ML";
 
 val pointer_eq = PolyML.pointerEq;