| changeset 61877 | 276ad4354069 |
| parent 59363 | 4660b0409096 |
| child 62663 | bea354f6ff21 |
--- a/src/Pure/General/path.ML Sun Dec 20 13:03:41 2015 +0100 +++ b/src/Pure/General/path.ML Sun Dec 20 13:06:26 2015 +0100 @@ -171,7 +171,7 @@ let val s = implode_path path in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end; -val print = Pretty.str_of o pretty; +val print = Pretty.unformatted_string_of o pretty; (* base element *)