src/Pure/Concurrent/timeout.ML
changeset 62923 3a122e1e352a
parent 62826 eb94e570c1a4
child 62924 ce47945ce4fb
--- a/src/Pure/Concurrent/timeout.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -17,7 +17,7 @@
 exception TIMEOUT of Time.time;
 
 fun apply timeout f x =
-  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+  Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
     let
       val self = Thread.self ();
       val start = Time.now ();
@@ -26,7 +26,7 @@
         Event_Timer.request (start + timeout)
           (fn () => Standard_Thread.interrupt_unsynchronized self);
       val result =
-        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
+        Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
 
       val stop = Time.now ();
       val was_timeout = not (Event_Timer.cancel request);