diff -r e43f0ea90c9a -r 0c4411e2fc90 src/Pure/Concurrent/par_exn.ML --- a/src/Pure/Concurrent/par_exn.ML Fri Aug 19 12:51:14 2011 +0200 +++ b/src/Pure/Concurrent/par_exn.ML Fri Aug 19 13:32:27 2011 +0200 @@ -22,7 +22,11 @@ fun serial exn = (case get_exn_serial exn of SOME i => (i, exn) - | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end); + | NONE => + let + val i = Library.serial (); + val exn' = uninterruptible (fn _ => set_exn_serial i) exn; + in (i, exn') end); val the_serial = the o get_exn_serial;