changeset 61877 | 276ad4354069 |
parent 58854 | b979c781c2db |
child 64776 | 3f20c63f71be |
--- a/src/Pure/General/url.ML Sun Dec 20 13:03:41 2015 +0100 +++ b/src/Pure/General/url.ML Sun Dec 20 13:06:26 2015 +0100 @@ -81,7 +81,7 @@ val pretty = Pretty.mark_str o `Markup.url o implode_url; -val print = Pretty.str_of o pretty; +val print = Pretty.unformatted_string_of o pretty; (*final declarations of this structure!*)