--- a/src/Pure/Concurrent/par_exn.ML Fri Dec 06 15:53:09 2019 +0100
+++ b/src/Pure/Concurrent/par_exn.ML Fri Dec 06 16:05:24 2019 +0100
@@ -7,7 +7,7 @@
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
--- a/src/Pure/ML/exn_properties.ML Fri Dec 06 15:53:09 2019 +0100
+++ b/src/Pure/ML/exn_properties.ML Fri Dec 06 16:05:24 2019 +0100
@@ -9,7 +9,7 @@
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 =