src/Pure/Concurrent/par_exn.ML
changeset 44271 89f40a5939b2
parent 44270 3eaad39e520c
child 44296 0c4411e2fc90
--- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 17:53:32 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 18:07:40 2011 +0200
@@ -9,7 +9,7 @@
 sig
   val serial: exn -> serial * exn
   val make: exn list -> exn
-  val dest: exn -> (serial * exn) list option
+  val dest: exn -> exn list option
   val release_all: 'a Exn.result list -> 'a list
   val release_first: 'a Exn.result list -> 'a list
 end;
@@ -43,7 +43,7 @@
     [] => Exn.Interrupt
   | es => Par_Exn es);
 
-fun dest (Par_Exn exns) = SOME (map (`the_serial) exns)
+fun dest (Par_Exn exns) = SOME exns
   | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;