changeset 39232 | 69c6d3e87660 |
parent 34293 | df93c72c0206 |
child 43761 | e72ba84ae58f |
--- 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);