diff -r 7325a5e3587f -r 228f27469139 src/Pure/Concurrent/lazy_sequential.ML
--- a/src/Pure/Concurrent/lazy_sequential.ML	Tue Jan 05 23:38:10 2010 +0100
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Wed Jan 06 13:14:28 2010 +0100
@@ -1,7 +1,8 @@
 (*  Title:      Pure/Concurrent/lazy_sequential.ML
     Author:     Florian Haftmann and Makarius, TU Muenchen
 
-Lazy evaluation with memoing (sequential version).
+Lazy evaluation with memoing of results and regular exceptions
+(sequential version).
 *)
 
 structure Lazy: LAZY =
@@ -28,9 +29,16 @@
 (* force result *)
 
 fun force_result (Lazy r) =
-  (case ! r of
-    Expr e => Exn.capture e ()
-  | Result res => res);
+  let
+    val result =
+      (case ! r of
+        Expr e => Exn.capture e ()
+      | Result res => res);
+    val _ =
+      (case result of
+        Exn.Exn Exn.Interrupt => ()
+      | _ => r := result);
+  in result end;
 
 fun force r = Exn.release (force_result r);