diff -r 14fd037ccc47 -r df93c72c0206 src/Pure/Concurrent/lazy_sequential.ML --- a/src/Pure/Concurrent/lazy_sequential.ML Thu Jan 07 17:41:06 2010 +0100 +++ b/src/Pure/Concurrent/lazy_sequential.ML Fri Jan 08 11:07:53 2010 +0100 @@ -37,7 +37,7 @@ val _ = (case result of Exn.Exn Exn.Interrupt => () - | _ => r := result); + | _ => r := Result result); in result end; fun force r = Exn.release (force_result r);