src/HOL/Tools/try0.ML

--- a/src/HOL/Tools/try0.ML	Mon Mar 10 15:04:01 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Mon Mar 10 15:20:41 2014 +0100
@@ -172,7 +172,7 @@
 
 fun string_of_xthm (xref, args) =
   Facts.string_of_ref xref ^
-  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src @{context}) args);
+  implode (map (enclose "[" "]" o Pretty.str_of o Args.pretty_src Pretty.str @{context}) args);
 
 val parse_fact_refs =
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse_Spec.xthm >> string_of_xthm));