tweaked verbose output

--- a/src/HOL/Sledgehammer.thy	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Sledgehammer.thy	Mon Jan 31 16:09:23 2022 +0100
@@ -36,6 +36,9 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
 (*
+lemma "1 + 1 = 3"
+  sledgehammer[verbose]
+
 lemma "1 + 1 = 2"
   sledgehammer [slices = 40, max_proofs = 40]
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -135,12 +135,20 @@
         (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play)))
 
 fun launch_prover (params as {verbose, spy, ...}) mode learn
-    (problem as {state, subgoal, factss, ...} : prover_problem) slice name =
+    (problem as {state, subgoal, factss, ...} : prover_problem)
+    (slice as ((num_facts, fact_filter), _)) name =
   let
     val ctxt = Proof.context_of state
 
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"))
 
+    val _ =
+      if verbose then
+        writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^
+          plural_s num_facts ^ "...")
+      else
+        ()
+
     fun print_used_facts used_facts used_from =
       tag_list 1 used_from
       |> map (fn (j, fact) => fact |> apsnd (K j))
@@ -164,7 +172,7 @@
           fun filter_info (fact_filter, facts) =
             let
               val indices = find_indices facts
-              (* "Int.max" is there for robustness -- it shouldn't be necessary *)
+              (* "Int.max" is there for robustness *)
               val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?"
             in
               (commas (indices @ unknowns), fact_filter)
@@ -182,11 +190,11 @@
       | spying_str_of_res {outcome = SOME failure, ...} =
         "Failure: " ^ string_of_atp_failure failure
  in
-  get_minimizing_prover ctxt mode learn name params problem slice
-  |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
-      print_used_facts used_facts used_from
-    | _ => ())
-  |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
+   get_minimizing_prover ctxt mode learn name params problem slice
+   |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
+       print_used_facts used_facts used_from
+     | _ => ())
+   |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
  end
 
 fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal
@@ -245,8 +253,7 @@
     val message = message ()
     val () =
       (case outcome of
-        SH_Some _ =>
-        the_default writeln writeln_result (prover_name ^ ": " ^ message)
+        SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message)
       | _ => ())
   in
     (outcome, message)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -73,7 +73,6 @@
       | NONE => (false, false))
     fun repair_context ctxt = ctxt
       |> Context.proof_map (SMT_Config.select_solver name)
-      |> Config.put SMT_Config.verbose debug
       |> Config.put SMT_Config.higher_order higher_order
       |> Config.put SMT_Config.nat_as_int nat_as_int
       |> (if overlord then