diff -r 7816e7be7bc7 -r ef3ec45ded4d src/HOL/Tools/try0_util.ML
--- a/src/HOL/Tools/try0_util.ML	Fri Mar 28 08:56:13 2025 +0100
+++ b/src/HOL/Tools/try0_util.ML	Fri Mar 28 16:09:20 2025 +0100
@@ -11,11 +11,10 @@
   val string_of_xref : Try0.xref -> string
 
   type facts_prefixes =
-    {usings: string,
-     simps : string,
-     intros : string,
-     elims : string,
-     dests : string}
+    {simps : string option,
+     intros : string option,
+     elims : string option,
+     dests : string option}
   val full_attrs : facts_prefixes
   val clas_attrs : facts_prefixes
   val simp_attrs : facts_prefixes
@@ -37,21 +36,21 @@
 
 
 type facts_prefixes =
-  {usings: string,
-   simps : string,
-   intros : string,
-   elims : string,
-   dests : string}
+  {simps : string option,
+   intros : string option,
+   elims : string option,
+   dests : string option}
 
 val no_attrs : facts_prefixes =
-  {usings = "", simps = "", intros = "", elims = "", dests = ""}
+  {simps = NONE, intros = NONE, elims = NONE, dests = NONE}
 val full_attrs : facts_prefixes =
-  {usings = "", simps = "simp", intros = "intro", elims = "elim", dests = "dest"}
+  {simps = SOME "simp: ", intros = SOME "intro: ", elims = SOME "elim: ", dests = SOME "dest: "}
 val clas_attrs : facts_prefixes =
-  {usings = "", simps = "", intros = "intro", elims = "elim", dests = "dest"}
+  {simps = NONE, intros = SOME "intro: ", elims = SOME "elim: ", dests = SOME "dest: "}
 val simp_attrs : facts_prefixes =
-  {usings = "", simps = "add", intros = "", elims = "", dests = ""}
-val metis_attrs : facts_prefixes = no_attrs
+  {simps = SOME "add: ", intros = NONE, elims = NONE, dests = NONE}
+val metis_attrs : facts_prefixes =
+  {simps = SOME "", intros = SOME "", elims = SOME "", dests = SOME ""}
 
 local
 
@@ -88,28 +87,36 @@
     val ctxt = Proof.context_of st
 
     val (unused_simps, simps_attrs) =
-      if #simps prefixes = "" then
-        (#simps facts, "")
+       if null (#simps facts) then
+        ([], "")
       else
-        ([], " " ^ #simps prefixes ^ ": " ^ space_implode "" (map string_of_xref (#simps facts)))
+        (case #simps prefixes of
+          NONE =>  (#simps facts, "")
+        | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#simps facts))))
 
     val (unused_intros, intros_attrs) =
-      if #intros prefixes = "" then
-        (#intros facts, "")
+      if null (#intros facts) then
+        ([], "")
       else
-        ([], " " ^ #intros prefixes ^ ": " ^ space_implode "" (map string_of_xref (#intros facts)))
+        (case #intros prefixes of
+          NONE =>  (#intros facts, "")
+        | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#intros facts))))
 
     val (unused_elims, elims_attrs) =
-      if #elims prefixes = "" then
-        (#elims facts, "")
+      if null (#elims facts) then
+        ([], "")
       else
-        ([], " " ^ #elims prefixes ^ ": " ^ space_implode "" (map string_of_xref (#elims facts)))
+        (case #elims prefixes of
+          NONE =>  (#elims facts, "")
+        | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#elims facts))))
 
     val (unused_dests, dests_attrs) =
-      if #dests prefixes = "" then
-        (#dests facts, "")
+      if null (#dests facts) then
+        ([], "")
       else
-        ([], " " ^ #dests prefixes ^ ": " ^ space_implode "" (map string_of_xref (#dests facts)))
+        (case #dests prefixes of
+          NONE =>  (#dests facts, "")
+        | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#dests facts))))
 
     val unused = #usings facts @ unused_simps @ unused_intros @ unused_elims @ unused_dests