src/Pure/General/pretty.ML
changeset 80875 2e33897071b6
parent 80873 e71cb37c7395
child 80878 cddd64134b49
--- a/src/Pure/General/pretty.ML	Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/General/pretty.ML	Thu Sep 12 19:52:01 2024 +0200
@@ -145,8 +145,8 @@
 fun mark_str (m, s) = mark m (str s);
 fun marks_str (ms, s) = fold_rev mark ms (str s);
 
-val mark_position = mark o Position.markup_position;
-fun mark_str_position (pos, s) = mark_str (Position.markup_position pos, s);
+val mark_position = mark o Position.markup;
+fun mark_str_position (pos, s) = mark_str (Position.markup pos, s);
 
 val item = markup Markup.item;
 val text_fold = markup Markup.text_fold;