src/Pure/Concurrent/timeout.ML
changeset 62826 eb94e570c1a4
parent 62519 a564458f94db
child 62923 3a122e1e352a
     1.1 --- a/src/Pure/Concurrent/timeout.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/timeout.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4        val start = Time.now ();
     1.5  
     1.6        val request =
     1.7 -        Event_Timer.request (Time.+ (start, timeout))
     1.8 +        Event_Timer.request (start + timeout)
     1.9            (fn () => Standard_Thread.interrupt_unsynchronized self);
    1.10        val result =
    1.11          Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
    1.12 @@ -33,7 +33,7 @@
    1.13        val test = Exn.capture Multithreading.interrupted ();
    1.14      in
    1.15        if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
    1.16 -      then raise TIMEOUT (Time.- (stop, start))
    1.17 +      then raise TIMEOUT (stop - start)
    1.18        else (Exn.release test; Exn.release result)
    1.19      end);
    1.20