src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

 
 (* Sledgehammer the given subgoal *)
 
 val default_learn_prover_timeout = 2.0
 
-fun hammer_away override_params subcommand opt_i fact_override state =
+fun hammer_away override_params subcommand opt_i fact_override state0 =
   let
+    val state = state0
+      |> Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false)
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 
     val override_params = override_params |> map (normalize_raw_param ctxt)
     val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))