merged

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Apr 24 22:45:04 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Apr 24 23:29:57 2025 +0200
@@ -44,6 +44,7 @@
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome ord
+  val try_command_line : string -> play_outcome -> string -> string
   val one_line_proof_text : one_line_params -> string
 end;
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Thu Apr 24 22:45:04 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Thu Apr 24 23:29:57 2025 +0200
@@ -84,25 +84,23 @@
       end
 
     val timer = Timer.startRealTimer ()
-    val out =
+    val (outcome, command) =
       (case run_try0 () of
-        NONE => SOME GaveUp
-      | SOME _ => NONE)
-      handle ERROR _ => SOME GaveUp
-           | Exn.Interrupt_Breakdown => SOME GaveUp
-           | Timeout.TIMEOUT _ => SOME TimedOut
+        NONE => (SOME GaveUp, "")
+      | SOME {command, ...} => (NONE, command))
+      handle ERROR _ => (SOME GaveUp, "")
+           | Exn.Interrupt_Breakdown => (SOME GaveUp, "")
+           | Timeout.TIMEOUT _ => (SOME TimedOut, "")
     val run_time = Timer.checkRealTimer timer
 
-    val (outcome, used_facts) =
-      (case out of
-        NONE => (found_something name; (NONE, map fst facts))
-      | some_failure => (some_failure, []))
+    val used_facts =
+      (case outcome of
+        NONE => (found_something name; map fst facts)
+      | SOME _ => [])
 
     val message = fn _ =>
       (case outcome of
-        NONE =>
-        one_line_proof_text ((map (apfst Pretty.str) used_facts, (meth_of name, Played run_time)),
-          proof_banner mode name, subgoal, subgoal_count)
+        NONE => try_command_line (proof_banner mode name) (Played run_time) command
       | SOME failure => string_of_atp_failure failure)
   in
     {outcome = outcome, used_facts = used_facts, used_from = facts,

--- a/src/HOL/Tools/try0_util.ML	Thu Apr 24 22:45:04 2025 +0200
+++ b/src/HOL/Tools/try0_util.ML	Thu Apr 24 23:29:57 2025 +0200
@@ -10,17 +10,18 @@
 sig
   val string_of_xref : Try0.xref -> string
 
-  type facts_prefixes =
-    {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
-  val metis_attrs : facts_prefixes
-  val no_attrs : facts_prefixes
-  val apply_raw_named_method : string -> bool -> facts_prefixes ->
+  type facts_config =
+    {usings_as_params : bool,
+     simps_prefix : string option,
+     intros_prefix : string option,
+     elims_prefix : string option,
+     dests_prefix : string option}
+  val full_attrs : facts_config
+  val clas_attrs : facts_config
+  val simp_attrs : facts_config
+  val metis_attrs : facts_config
+  val no_attrs : facts_config
+  val apply_raw_named_method : string -> bool -> facts_config ->
     (Proof.context -> Proof.context) -> Time.time option -> Try0.facts -> Proof.state ->
     Try0.result option
 end
@@ -34,23 +35,43 @@
       Facts.string_of_ref xref) ^ implode
         (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
 
-
-type facts_prefixes =
-  {simps : string option,
-   intros : string option,
-   elims : string option,
-   dests : string option}
+type facts_config =
+  {usings_as_params : bool,
+   simps_prefix : string option,
+   intros_prefix : string option,
+   elims_prefix : string option,
+   dests_prefix : string option}
 
-val no_attrs : facts_prefixes =
-  {simps = NONE, intros = NONE, elims = NONE, dests = NONE}
-val full_attrs : facts_prefixes =
-  {simps = SOME "simp: ", intros = SOME "intro: ", elims = SOME "elim: ", dests = SOME "dest: "}
-val clas_attrs : facts_prefixes =
-  {simps = NONE, intros = SOME "intro: ", elims = SOME "elim: ", dests = SOME "dest: "}
-val simp_attrs : facts_prefixes =
-  {simps = SOME "add: ", intros = NONE, elims = NONE, dests = NONE}
-val metis_attrs : facts_prefixes =
-  {simps = SOME "", intros = SOME "", elims = SOME "", dests = SOME ""}
+val no_attrs : facts_config =
+  {usings_as_params = false,
+   simps_prefix = NONE,
+   intros_prefix = NONE,
+   elims_prefix = NONE,
+   dests_prefix = NONE}
+val full_attrs : facts_config =
+  {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 =
+  {usings_as_params = false,
+   simps_prefix = NONE,
+   intros_prefix = SOME "intro: ",
+   elims_prefix = SOME "elim: ",
+   dests_prefix = SOME "dest: "}
+val simp_attrs : facts_config =
+  {usings_as_params = false,
+   simps_prefix = SOME "add: ",
+   intros_prefix = NONE,
+   elims_prefix = NONE,
+   dests_prefix = NONE}
+val metis_attrs : facts_config =
+  {usings_as_params = true,
+   simps_prefix = SOME "",
+   intros_prefix = SOME "",
+   elims_prefix = SOME "",
+   dests_prefix = SOME ""}
 
 local
 
@@ -79,7 +100,7 @@
 
 in
 
-fun apply_raw_named_method (name : string) all_goals (prefixes: facts_prefixes)
+fun apply_raw_named_method (name : string) all_goals (facts_config: facts_config)
   (silence_methods : Proof.context -> Proof.context) timeout_opt (facts : Try0.facts)
   (st : Proof.state) : Try0.result option =
   let
@@ -90,37 +111,45 @@
        if null (#simps facts) then
         ([], "")
       else
-        (case #simps prefixes of
+        (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
         ([], "")
       else
-        (case #intros prefixes of
+        (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
         ([], "")
       else
-        (case #elims prefixes of
+        (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
         ([], "")
       else
-        (case #dests prefixes of
+        (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
@@ -150,4 +179,4 @@
 
 end
 
-end
\ No newline at end of file
+end