| changeset 71250 | bd93c71521a0 |
| parent 62923 | 3a122e1e352a |
| child 77776 | 58e53c61f15f |
--- 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 =