changeset 80875 | 2e33897071b6 |
parent 80873 | e71cb37c7395 |
child 81218 | 94bace5078ba |
--- a/src/Pure/Syntax/term_position.ML Thu Sep 12 19:46:08 2024 +0200 +++ b/src/Pure/Syntax/term_position.ML Thu Sep 12 19:52:01 2024 +0200 @@ -29,7 +29,7 @@ fun pretty pos = Pretty.mark_str_position (pos, position_dummy); fun encode pos = - YXML.string_of (XML.Elem (Position.markup_position pos, [position_text])); + YXML.string_of (XML.Elem (Position.markup pos, [position_text])); fun decode str = (case YXML.parse_body str handle Fail msg => error msg of