more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;
--- 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;