# HG changeset patch
# User wenzelm
# Date 1727192465 -7200
# Node ID 3eca969b3c43bce3ec6194dc53ca125c5d78aab9
# Parent  a119154a5f27a2d2cd2293a25f828bd66ddbc966
tuned;

diff -r a119154a5f27 -r 3eca969b3c43 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue Sep 24 17:35:24 2024 +0200
+++ b/src/Pure/General/binding.ML	Tue Sep 24 17:41:05 2024 +0200
@@ -177,7 +177,7 @@
 fun pretty b =
   if is_empty b then Pretty.str "\"\""
   else
-    Pretty.mark (Position.markup_properties (pos_of b) Markup.binding) (Pretty.str (long_name_of b))
+    Pretty.mark_str (Position.markup_properties (pos_of b) Markup.binding, long_name_of b)
     |> Pretty.quote;
 
 val print = Pretty.unformatted_string_of o pretty;
diff -r a119154a5f27 -r 3eca969b3c43 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Tue Sep 24 17:35:24 2024 +0200
+++ b/src/Pure/Tools/find_consts.ML	Tue Sep 24 17:41:05 2024 +0200
@@ -65,7 +65,7 @@
     val markup = Name_Space.markup (Proof_Context.const_space ctxt) c;
   in
     Pretty.block
-     [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
+     [Pretty.mark_str (markup, c), Pretty.str " ::", Pretty.brk 1,
       Pretty.quote (Syntax.pretty_typ ctxt ty')]
   end;