--- a/src/HOL/Tools/try0.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/try0.ML Fri Jan 04 23:22:53 2019 +0100
@@ -172,7 +172,7 @@
fun string_of_xthm (xref, args) =
Facts.string_of_ref xref ^
- implode (map (enclose "[" "]" o Pretty.unformatted_string_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.thm >> string_of_xthm));