diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/event_timer.ML --- a/src/Pure/Concurrent/event_timer.ML Sat Apr 09 13:28:32 2016 +0200 +++ b/src/Pure/Concurrent/event_timer.ML Sat Apr 09 14:00:23 2016 +0200 @@ -109,7 +109,7 @@ manager_loop); fun shutdown () = - Multithreading.uninterruptible (fn restore_attributes => fn () => + Thread_Attributes.uninterruptible (fn restore_attributes => fn () => if Synchronized.change_result state (fn st as State {requests, manager, ...} => if is_shutdown Normal st then (false, st) else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then @@ -144,7 +144,7 @@ val manager' = manager_check manager; in (canceled, make_state (requests', status, manager')) end); -val future = Multithreading.uninterruptible (fn _ => fn time => +val future = Thread_Attributes.uninterruptible (fn _ => fn time => let val req: request Single_Assignment.var = Single_Assignment.var "request"; fun abort () = ignore (cancel (Single_Assignment.await req));