src/Pure/ROOT.ML
changeset 54717 42c209a6c225
parent 54449 f3cfe882f9af
child 54740 91f54d386680
--- a/src/Pure/ROOT.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/ROOT.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -76,10 +76,13 @@
 else use "ML/exn_properties_dummy.ML";
 
 if ML_System.name = "polyml-5.5.1"
+  orelse ML_System.name = "polyml-5.5.2"
 then use "ML/exn_trace_polyml-5.5.1.ML"
 else ();
 
-if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1"
+if ML_System.name = "polyml-5.5.0"
+  orelse ML_System.name = "polyml-5.5.1"
+  orelse ML_System.name = "polyml-5.5.2"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";
 
@@ -347,5 +350,4 @@
 val cd = File.cd o Path.explode;
 
 Proofterm.proofs := 0;
-Multithreading.max_threads := 0;