src/Pure/ROOT.ML
changeset 43948 8f5add916a99
parent 43850 7f2cbc713344
child 44062 55a4df7f2568
--- a/src/Pure/ROOT.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/ROOT.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -62,9 +62,7 @@
 use "General/binding.ML";
 
 use "General/sha1.ML";
-if String.isPrefix "polyml" ml_system
-then use "General/sha1_polyml.ML"
-else ();
+if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
 
 
 (* concurrency within the ML runtime *)
@@ -73,8 +71,7 @@
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";
 
-if String.isPrefix "smlnj" ml_system then ()
-else use "Concurrent/time_limit.ML";
+if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML";
 
 if Multithreading.available
 then use "Concurrent/bash.ML"
@@ -191,7 +188,7 @@
 use "ML/ml_env.ML";
 use "Isar/runtime.ML";
 use "ML/ml_compiler.ML";
-if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then ()
+if ML_System.name = "polyml-5.2.1" orelse ML_System.is_smlnj then ()
 else use "ML/ml_compiler_polyml-5.3.ML";
 use "ML/ml_context.ML";