# HG changeset patch # User Fabian Huch # 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