| changeset 77776 | 58e53c61f15f |
| parent 71250 | bd93c71521a0 |
| child 78679 | dc7455787a8e |
--- a/src/Pure/ML/exn_properties.ML Sat Apr 01 19:15:38 2023 +0200 +++ b/src/Pure/ML/exn_properties.ML Sat Apr 01 21:12:44 2023 +0200 @@ -26,7 +26,7 @@ | body => XML.Decode.properties body); fun position_of_polyml_location loc = - Position.make + Position.of_props {line = FixedInt.toInt (#startLine loc), offset = FixedInt.toInt (#startPosition loc), end_offset = FixedInt.toInt (#endPosition loc),