src/Pure/Concurrent/time_limit.ML

--- a/src/Pure/Concurrent/time_limit.ML	Fri May 17 21:15:33 2013 +0200
+++ b/src/Pure/Concurrent/time_limit.ML	Fri May 17 23:31:02 2013 +0200
@@ -28,9 +28,11 @@
         Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
 
       val was_timeout = not (Event_Timer.cancel request);
+      val test = Exn.capture Multithreading.interrupted ();
     in
-      if was_timeout andalso Exn.is_interrupt_exn result
+      if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
       then raise TimeOut
+      else if Exn.is_interrupt_exn test then Exn.interrupt ()
       else Exn.release result
     end);