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;