src/Pure/ROOT.ML
changeset 62889 99c7f31615c2
parent 62883 b04e9fe29223
child 62890 728aa05e9433
     1.1 --- a/src/Pure/ROOT.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4  use "General/exn.ML";
     1.5  
     1.6  use "Concurrent/multithreading.ML";
     1.7 +use "Concurrent/thread_data.ML";
     1.8  use "Concurrent/unsynchronized.ML";
     1.9  
    1.10  use "ML/ml_heap.ML";