src/Pure/ROOT.ML
changeset 59054 61b723761dff
parent 59026 30b8a5825a9c
child 59064 a8bcb5a446c8
     1.1 --- a/src/Pure/ROOT.ML	Tue Nov 25 17:30:05 2014 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Nov 26 11:43:51 2014 +0100
     1.3 @@ -18,8 +18,6 @@
     1.4  use "General/alist.ML";
     1.5  use "General/table.ML";
     1.6  
     1.7 -use "Concurrent/simple_thread.ML";
     1.8 -
     1.9  use "Concurrent/synchronized.ML";
    1.10  if Multithreading.available then ()
    1.11  else use "Concurrent/synchronized_sequential.ML";
    1.12 @@ -51,6 +49,7 @@
    1.13  val toplevel_pp = Secure.toplevel_pp;
    1.14  
    1.15  
    1.16 +
    1.17  (** bootstrap phase 1: towards ML within Isar context *)
    1.18  
    1.19  (* library of general tools *)
    1.20 @@ -107,6 +106,8 @@
    1.21  then use "ML/ml_statistics_polyml-5.5.0.ML"
    1.22  else use "ML/ml_statistics_dummy.ML";
    1.23  
    1.24 +use "Concurrent/simple_thread.ML";
    1.25 +
    1.26  use "Concurrent/single_assignment.ML";
    1.27  if Multithreading.available then ()
    1.28  else use "Concurrent/single_assignment_sequential.ML";