src/Pure/ROOT.ML
changeset 62354 fdd6989cc8a0
parent 61794 4c232a2ddeab
child 62355 00f7618a9f2b
     1.1 --- a/src/Pure/ROOT.ML	Wed Feb 17 21:08:18 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Feb 17 23:06:24 2016 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4  use "General/timing.ML";
     1.5  
     1.6  use "General/sha1.ML";
     1.7 -if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
     1.8 +use "General/sha1_polyml.ML";
     1.9  use "General/sha1_samples.ML";
    1.10  
    1.11  use "PIDE/yxml.ML";
    1.12 @@ -98,9 +98,7 @@
    1.13  
    1.14  (* concurrency within the ML runtime *)
    1.15  
    1.16 -if ML_System.is_polyml
    1.17 -then use "ML/exn_properties_polyml.ML"
    1.18 -else use "ML/exn_properties_dummy.ML";
    1.19 +use "ML/exn_properties_polyml.ML";
    1.20  
    1.21  if ML_System.name = "polyml-5.5.0"
    1.22    orelse ML_System.name = "polyml-5.5.1"
    1.23 @@ -123,8 +121,7 @@
    1.24  use "Concurrent/task_queue.ML";
    1.25  use "Concurrent/future.ML";
    1.26  use "Concurrent/event_timer.ML";
    1.27 -
    1.28 -if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
    1.29 +use "Concurrent/time_limit.ML";
    1.30  
    1.31  use "Concurrent/lazy.ML";
    1.32  if Multithreading.available then ()
    1.33 @@ -203,13 +200,11 @@
    1.34  use "ML/ml_syntax.ML";
    1.35  use "ML/ml_env.ML";
    1.36  use "ML/ml_options.ML";
    1.37 -use "ML/exn_output.ML";
    1.38 -if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
    1.39 +use "ML/exn_output_polyml.ML";
    1.40  use "ML/ml_options.ML";
    1.41  use "Isar/runtime.ML";
    1.42  use "PIDE/execution.ML";
    1.43 -use "ML/ml_compiler.ML";
    1.44 -if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
    1.45 +use "ML/ml_compiler_polyml.ML";
    1.46  
    1.47  use "skip_proof.ML";
    1.48  use "goal.ML";
    1.49 @@ -359,7 +354,7 @@
    1.50  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
    1.51  toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
    1.52  
    1.53 -if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
    1.54 +use "ML/install_pp_polyml.ML";
    1.55  
    1.56  
    1.57  (* the Pure theory *)