# HG changeset patch
# User wenzelm
# Date 1226744717 -3600
# Node ID 56cb4130177aa9cbc6cdf917bafd7bfbfceac79f
# Parent  6891e273c33bcf1f6640b850ef62559a52a49d96
multithreading support for polyml-5.2 actually disabled -- as advertized;

diff -r 6891e273c33b -r 56cb4130177a src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Fri Nov 14 16:49:52 2008 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Nov 15 11:25:17 2008 +0100
@@ -7,7 +7,8 @@
 open Thread;
 use "ML-Systems/polyml_common.ML";
 
-if ml_system = "polyml-5.2" then ()
+if ml_system = "polyml-5.2"
+then use "ML-Systems/thread_dummy.ML"
 else use "ML-Systems/multithreading_polyml.ML";
 
 val pointer_eq = PolyML.pointerEq;