src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

                  run_time_in_msecs = run_time_in_msecs, preplay = preplay,
                  message = message})
              | NONE => result
            end)
 
-fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
-                              expect, ...})
+fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
+                              timeout, expect, ...})
         mode minimize_command only
         {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
   let
     val ctxt = Proof.context_of state
     val hard_timeout = Time.+ (timeout, timeout)

         (outcome_code, state)
       end
     else
       (Async_Manager.launch das_tool birth_time death_time (desc ())
                             ((fn (outcome_code, message) =>
-                                 (outcome_code = someN, message ())) o go);
+                                 (verbose orelse outcome_code = someN,
+                                  message ())) o go);
        (unknownN, state))
   end
 
 fun class_of_smt_solver ctxt name =
   ctxt |> select_smt_solver name