| changeset 61877 | 276ad4354069 |
| parent 61267 | 0b6217fda81b |
| child 61878 | fa4dbb82732f |
--- a/src/Pure/context.ML Sun Dec 20 13:03:41 2015 +0100 +++ b/src/Pure/context.ML Sun Dec 20 13:06:26 2015 +0100 @@ -179,7 +179,7 @@ val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names; in Pretty.str_list "{" "}" abbrev end; -val str_of_thy = Pretty.str_of o pretty_abbrev_thy; +val str_of_thy = Pretty.unformatted_string_of o pretty_abbrev_thy; fun get_theory thy name = if theory_name thy <> name then