src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Thu May 24 15:01:17 2012 +0200
+++ b/src/Pure/ROOT.ML	Thu May 24 15:33:45 2012 +0200
@@ -74,7 +74,7 @@
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";
 
-if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML";
+if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
 
 if Multithreading.available
 then use "Concurrent/bash.ML"
@@ -191,8 +191,7 @@
 use "ML/ml_env.ML";
 use "Isar/runtime.ML";
 use "ML/ml_compiler.ML";
-if ML_System.is_smlnj then ()
-else use "ML/ml_compiler_polyml-5.3.ML";
+if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
 use "ML/ml_context.ML";
 
 (*theory sources*)