src/Pure/ROOT.ML
changeset 43948 8f5add916a99
parent 43850 7f2cbc713344
child 44062 55a4df7f2568
     1.1 --- a/src/Pure/ROOT.ML	Sat Jul 23 16:37:17 2011 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Sat Jul 23 17:22:28 2011 +0200
     1.3 @@ -62,9 +62,7 @@
     1.4  use "General/binding.ML";
     1.5  
     1.6  use "General/sha1.ML";
     1.7 -if String.isPrefix "polyml" ml_system
     1.8 -then use "General/sha1_polyml.ML"
     1.9 -else ();
    1.10 +if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
    1.11  
    1.12  
    1.13  (* concurrency within the ML runtime *)
    1.14 @@ -73,8 +71,7 @@
    1.15  if Multithreading.available then ()
    1.16  else use "Concurrent/single_assignment_sequential.ML";
    1.17  
    1.18 -if String.isPrefix "smlnj" ml_system then ()
    1.19 -else use "Concurrent/time_limit.ML";
    1.20 +if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML";
    1.21  
    1.22  if Multithreading.available
    1.23  then use "Concurrent/bash.ML"
    1.24 @@ -191,7 +188,7 @@
    1.25  use "ML/ml_env.ML";
    1.26  use "Isar/runtime.ML";
    1.27  use "ML/ml_compiler.ML";
    1.28 -if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then ()
    1.29 +if ML_System.name = "polyml-5.2.1" orelse ML_System.is_smlnj then ()
    1.30  else use "ML/ml_compiler_polyml-5.3.ML";
    1.31  use "ML/ml_context.ML";
    1.32