# HG changeset patch
# User blanchet
# Date 1643641763 -3600
# Node ID 46e3a423a7871126ad0c4698f9203eae100153f8
# Parent  212e9ec706cf5bd9aef65968160817f5d4a7e092
print more verbose information

diff -r 212e9ec706cf -r 46e3a423a787 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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
@@ -423,6 +423,12 @@
               if mode = Auto_Try then provers
               else schedule_of_provers provers slices
             val prover_slices = prover_slices_of_schedule ctxt params schedule
+
+            val _ =
+              if verbose then
+                writeln ("Running " ^ commas (map fst prover_slices) ^ "...")
+              else
+                ()
           in
             if mode = Auto_Try then
               (SH_Unknown, "")