tuned;

--- a/src/Pure/Concurrent/time_limit.ML	Mon May 20 16:17:56 2013 +0200
+++ b/src/Pure/Concurrent/time_limit.ML	Mon May 20 17:10:33 2013 +0200
@@ -32,8 +32,7 @@
     in
       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
+      else (Exn.release test; Exn.release result)
     end);
 
 end;