# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1729790029 -7200
# Node ID daf5697035b5ecc4c2a5eed8d81ab4ca53f397df
# Parent  0677712016b56bbb2486699d49238992ee0a306a
try0: support literal facts;

diff -r 0677712016b5 -r daf5697035b5 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Oct 24 16:46:25 2024 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Oct 24 19:13:49 2024 +0200
@@ -47,8 +47,8 @@
 datatype modifier = Use | Simp | Intro | Elim | Dest
 
 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)
+  (case xref of Facts.Fact literal => cartouche literal | _ => Facts.string_of_ref xref) ^
+    implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
 
 fun add_attr_text tagged (tag, src) s =
   let