# HG changeset patch
# User wenzelm
# Date 1248990611 -7200
# Node ID d00238af17b69db99ac88c109afefa25e960512d
# Parent  e0b8da3fae4db4ec86053aa4ba3f7ef7696f87a3
recovered polyml-5.2 -- need to reload ML-Systems/multithreading.ML after overriding Thread structures;

diff -r e0b8da3fae4d -r d00238af17b6 src/Pure/ML-Systems/polyml.ML
--- 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;