# HG changeset patch
# User desharna
# Date 1745501388 -7200
# Node ID cf21066637d7f6a6e9996ecbfed567de7b4d253c
# Parent  f3b3d49d84d702efcdc4fea3b939138c60644832
pass "using" facts as parameters to metis in try0

diff -r f3b3d49d84d7 -r cf21066637d7 src/HOL/Tools/try0_util.ML
--- a/src/HOL/Tools/try0_util.ML	Thu Apr 24 14:53:32 2025 +0200
+++ b/src/HOL/Tools/try0_util.ML	Thu Apr 24 15:29:48 2025 +0200
@@ -11,7 +11,8 @@
   val string_of_xref : Try0.xref -> string
 
   type facts_config =
-    {simps_prefix : string option,
+    {usings_as_params : bool,
+     simps_prefix : string option,
      intros_prefix : string option,
      elims_prefix : string option,
      dests_prefix : string option}
@@ -35,33 +36,39 @@
         (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
 
 type facts_config =
-  {simps_prefix : string option,
+  {usings_as_params : bool,
+   simps_prefix : string option,
    intros_prefix : string option,
    elims_prefix : string option,
    dests_prefix : string option}
 
 val no_attrs : facts_config =
-  {simps_prefix = NONE,
+  {usings_as_params = false,
+   simps_prefix = NONE,
    intros_prefix = NONE,
    elims_prefix = NONE,
    dests_prefix = NONE}
 val full_attrs : facts_config =
-  {simps_prefix = SOME "simp: ",
+  {usings_as_params = false,
+   simps_prefix = SOME "simp: ",
    intros_prefix = SOME "intro: ",
    elims_prefix = SOME "elim: ",
    dests_prefix = SOME "dest: "}
 val clas_attrs : facts_config =
-  {simps_prefix = NONE,
+  {usings_as_params = false,
+   simps_prefix = NONE,
    intros_prefix = SOME "intro: ",
    elims_prefix = SOME "elim: ",
    dests_prefix = SOME "dest: "}
 val simp_attrs : facts_config =
-  {simps_prefix = SOME "add: ",
+  {usings_as_params = false,
+   simps_prefix = SOME "add: ",
    intros_prefix = NONE,
    elims_prefix = NONE,
    dests_prefix = NONE}
 val metis_attrs : facts_config =
-  {simps_prefix = SOME "",
+  {usings_as_params = true,
+   simps_prefix = SOME "",
    intros_prefix = SOME "",
    elims_prefix = SOME "",
    dests_prefix = SOME ""}
@@ -106,7 +113,7 @@
       else
         (case #simps_prefix facts_config of
           NONE =>  (#simps facts, "")
-        | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#simps facts))))
+        | SOME prefix => ([], " " ^ prefix ^ implode_space (map string_of_xref (#simps facts))))
 
     val (unused_intros, intros_attrs) =
       if null (#intros facts) then
@@ -114,7 +121,7 @@
       else
         (case #intros_prefix facts_config of
           NONE =>  (#intros facts, "")
-        | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#intros facts))))
+        | SOME prefix => ([], " " ^ prefix ^ implode_space (map string_of_xref (#intros facts))))
 
     val (unused_elims, elims_attrs) =
       if null (#elims facts) then
@@ -122,7 +129,7 @@
       else
         (case #elims_prefix facts_config of
           NONE =>  (#elims facts, "")
-        | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#elims facts))))
+        | SOME prefix => ([], " " ^ prefix ^ implode_space (map string_of_xref (#elims facts))))
 
     val (unused_dests, dests_attrs) =
       if null (#dests facts) then
@@ -130,11 +137,19 @@
       else
         (case #dests_prefix facts_config of
           NONE =>  (#dests facts, "")
-        | SOME prefix => ([], " " ^ prefix ^ space_implode "" (map string_of_xref (#dests facts))))
+        | SOME prefix => ([], " " ^ prefix ^ implode_space (map string_of_xref (#dests facts))))
 
-    val unused = #usings facts @ unused_simps @ unused_intros @ unused_elims @ unused_dests
+    val (unused_usings, using_attrs) =
+      if null (#usings facts) then
+        ([], "")
+      else if #usings_as_params facts_config then
+        ([], " " ^ implode_space (map string_of_xref (#usings facts)))
+      else
+        (#usings facts, "")
 
-    val attrs = simps_attrs ^ intros_attrs ^ elims_attrs ^ dests_attrs
+    val unused = unused_simps @ unused_intros @ unused_elims @ unused_dests @ unused_usings
+
+    val attrs = simps_attrs ^ intros_attrs ^ elims_attrs ^ dests_attrs ^ using_attrs
     val text =
       name ^ attrs
       |> parse_method ctxt