src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/ROOT.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -70,6 +70,10 @@
 
 (* concurrency within the ML runtime *)
 
+if ML_System.is_polyml
+then use "ML/exn_properties_polyml.ML"
+else use "ML/exn_properties_dummy.ML";
+
 if ML_System.name = "polyml-5.5.0"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";