src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
                 SOME name => error ("No such prover: " ^ name ^ ".")
               | NONE => ()
       val _ = print "Sledgehammering..."
-      val _ = spying spy (fn () => ("***", "run"))
+      val _ = spying spy (fn () => ("***", "starting " ^ @{make_string} mode ^ " mode"))
       val (smts, (ueq_atps, full_atps)) =
         provers |> List.partition (is_smt_prover ctxt)
                 ||> List.partition (is_unit_equational_atp ctxt)
 
       val spying_str_of_factss =