src/Pure/Syntax/term_position.ML
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