src/Pure/ROOT.ML
changeset 52050 b40ed9dcf903
parent 52009 3b18ef9df768
child 52059 2f970c7f722b
     1.1 --- a/src/Pure/ROOT.ML	Fri May 17 13:46:18 2013 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri May 17 17:11:06 2013 +0200
     1.3 @@ -72,6 +72,8 @@
     1.4  
     1.5  (* concurrency within the ML runtime *)
     1.6  
     1.7 +use "Concurrent/event_timer.ML";
     1.8 +
     1.9  if ML_System.is_polyml
    1.10  then use "ML/exn_properties_polyml.ML"
    1.11  else use "ML/exn_properties_dummy.ML";