1.1 --- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 17:30:47 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 17:53:32 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val serial: exn -> serial * exn
     1.6    val make: exn list -> exn
     1.7 -  val dest: exn -> exn list option
     1.8 +  val dest: exn -> (serial * exn) list option
     1.9    val release_all: 'a Exn.result list -> 'a list
    1.10    val release_first: 'a Exn.result list -> 'a list
    1.11  end;
    1.12 @@ -24,7 +24,9 @@
    1.13      SOME i => (i, exn)
    1.14    | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
    1.15  
    1.16 -val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
    1.17 +val the_serial = the o get_exn_serial;
    1.18 +
    1.19 +val exn_ord = rev_order o int_ord o pairself the_serial;
    1.20  
    1.21  
    1.22  (* parallel exceptions *)
    1.23 @@ -41,8 +43,8 @@
    1.24      [] => Exn.Interrupt
    1.25    | es => Par_Exn es);
    1.26  
    1.27 -fun dest (Par_Exn exns) = SOME exns
    1.28 -  | dest _ = NONE;
    1.29 +fun dest (Par_Exn exns) = SOME (map (`the_serial) exns)
    1.30 +  | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
    1.31  
    1.32  
    1.33  (* parallel results *)