diff --git a/src/Pure/Concurrent/par_exn.ML b/src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML
+++ b/src/Pure/Concurrent/par_exn.ML
@@ -1,79 +1,79 @@
 (*  Title:      Pure/Concurrent/par_exn.ML
     Author:     Makarius
 
 Parallel exceptions as flattened results from acyclic graph of
 evaluations.  Interrupt counts as neutral element.
 *)
 
 signature PAR_EXN =
 sig
-  val identify: Properties.entry list -> exn -> exn
+  val identify: Properties.T -> exn -> exn
   val the_serial: exn -> int
   val make: exn list -> exn
   val dest: exn -> exn list option
   val is_interrupted: 'a Exn.result list -> bool
   val release_all: 'a Exn.result list -> 'a list
   val release_first: 'a Exn.result list -> 'a list
 end;
 
 structure Par_Exn: PAR_EXN =
 struct
 
 (* identification via serial numbers -- NOT portable! *)
 
 fun identify default_props exn =
   let
     val props = Exn_Properties.get exn;
     val update_serial =
       if Properties.defined props Markup.serialN then []
       else [(Markup.serialN, serial_string ())];
     val update_props = filter_out (Properties.defined props o #1) default_props;
   in Exn_Properties.update (update_serial @ update_props) exn end;
 
 fun the_serial exn =
   Value.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
 
 val exn_ord = rev_order o int_ord o apply2 the_serial;
 
 
 (* parallel exceptions *)
 
 exception Par_Exn of exn list;
   (*non-empty list with unique identified elements sorted by exn_ord;
     no occurrences of Par_Exn or Exn.Interrupt*)
 
 fun par_exns (Par_Exn exns) = exns
   | par_exns exn = if Exn.is_interrupt exn then [] else [identify [] exn];
 
 fun make exns =
   let
     val exnss = map par_exns exns;
     val exns' = Ord_List.unions exn_ord exnss handle Option.Option => flat exnss;
   in if null exns' then Exn.Interrupt else Par_Exn exns' end;
 
 fun dest (Par_Exn exns) = SOME exns
   | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
 
 
 (* parallel results *)
 
 fun is_interrupted results =
   exists (fn Exn.Exn _ => true | _ => false) results andalso
     Exn.is_interrupt (make (map_filter Exn.get_exn results));
 
 fun release_all results =
   if forall (fn Exn.Res _ => true | _ => false) results
   then map Exn.release results
   else raise make (map_filter Exn.get_exn results);
 
 fun plain_exn (Exn.Res _) = NONE
   | plain_exn (Exn.Exn (Par_Exn _)) = NONE
   | plain_exn (Exn.Exn exn) = if Exn.is_interrupt exn then NONE else SOME exn;
 
 fun release_first results =
   (case get_first plain_exn results of
     NONE => release_all results
   | SOME exn => Exn.reraise exn);
 
 end;
 
diff --git a/src/Pure/ML/exn_properties.ML b/src/Pure/ML/exn_properties.ML
--- a/src/Pure/ML/exn_properties.ML
+++ b/src/Pure/ML/exn_properties.ML
@@ -1,71 +1,71 @@
 (*  Title:      Pure/ML/exn_properties.ML
     Author:     Makarius
 
 Exception properties.
 *)
 
 signature EXN_PROPERTIES =
 sig
   val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T
   val position: exn -> Position.T
   val get: exn -> Properties.T
-  val update: Properties.entry list -> exn -> exn
+  val update: Properties.T -> exn -> exn
 end;
 
 structure Exn_Properties: EXN_PROPERTIES =
 struct
 
 (* source locations *)
 
 fun props_of_polyml_location (loc: ML_Compiler0.polyml_location) =
   (case YXML.parse_body (#file loc) of
     [] => []
   | [XML.Text file] =>
       if file = "Standard Basis" then []
       else [(Markup.fileN, ML_System.standard_path file)]
   | body => XML.Decode.properties body);
 
 fun position_of_polyml_location loc =
   Position.make
    {line = FixedInt.toInt (#startLine loc),
     offset = FixedInt.toInt (#startPosition loc),
     end_offset = FixedInt.toInt (#endPosition loc),
     props = props_of_polyml_location loc};
 
 fun position exn =
   (case Exn.polyml_location exn of
     NONE => Position.none
   | SOME loc => position_of_polyml_location loc);
 
 
 (* exception properties *)
 
 fun get exn =
   (case Exn.polyml_location exn of
     NONE => []
   | SOME loc => props_of_polyml_location loc);
 
 fun update entries exn =
   if Exn.is_interrupt exn then exn
   else
     let
       val loc =
         the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
           (Exn.polyml_location exn);
       val props = props_of_polyml_location loc;
       val props' = fold Properties.put entries props;
     in
       if props = props' then exn
       else
         let
           val loc' =
             {file = YXML.string_of_body (XML.Encode.properties props'),
               startLine = #startLine loc, endLine = #endLine loc,
               startPosition = #startPosition loc, endPosition = #endPosition loc};
         in
           Thread_Attributes.uninterruptible (fn _ => fn () =>
             PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
         end
     end;
 
 end;