src/Pure/General/binding.ML
changeset 80939 3eca969b3c43
parent 80876 55b74d63b18c
--- 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;