src/Pure/ROOT.ML
changeset 62519 a564458f94db
parent 62516 5732f1c31566
child 62551 df62e1ab7d88
     1.1 --- a/src/Pure/ROOT.ML	Sat Mar 05 13:57:25 2016 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Sat Mar 05 17:01:45 2016 +0100
     1.3 @@ -203,7 +203,7 @@
     1.4  use "Concurrent/task_queue.ML";
     1.5  use "Concurrent/future.ML";
     1.6  use "Concurrent/event_timer.ML";
     1.7 -use "Concurrent/time_limit.ML";
     1.8 +use "Concurrent/timeout.ML";
     1.9  use "Concurrent/lazy.ML";
    1.10  use "Concurrent/par_list.ML";
    1.11