src/Pure/Concurrent/lazy_sequential.ML

--- a/src/Pure/Concurrent/lazy_sequential.ML	Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Thu Sep 09 17:20:27 2010 +0200
@@ -34,10 +34,7 @@
       (case ! r of
         Expr e => Exn.capture e ()
       | Result res => res);
-    val _ =
-      (case result of
-        Exn.Exn Exn.Interrupt => ()
-      | _ => r := Result result);
+    val _ = if Exn.is_interrupt_exn result then () else r := Result result;
   in result end;
 
 fun force r = Exn.release (force_result r);