# HG changeset patch
# User wenzelm
# Date 1369062633 -7200
# Node ID 5534ec8b90a91955a7f23ff339b2df590a0c1aa7
# Parent  573e80625c78d667a982487fcf663c88cd932947
tuned;

diff -r 573e80625c78 -r 5534ec8b90a9 src/Pure/Concurrent/time_limit.ML
--- 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;