| changeset 61877 | 276ad4354069 |
| parent 61841 | 4d3527b94f2a |
| child 62519 | a564458f94db |
--- a/src/HOL/Tools/try0.ML Sun Dec 20 13:03:41 2015 +0100 +++ b/src/HOL/Tools/try0.ML Sun Dec 20 13:06:26 2015 +0100 @@ -163,7 +163,7 @@ fun string_of_xthm (xref, args) = Facts.string_of_ref xref ^ - implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args); + implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src @{context}) args); val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));