src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

       | Algebra_Method => "algebra")
   in
     maybe_paren (space_implode " " (meth_s :: ss))
   end
 
-val silence_methods = Try0.silence_methods false
-
 fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
   Method.insert_tac local_facts THEN'
   (case meth of
     Metis_Method (type_enc_opt, lam_trans_opt) =>
     let val ctxt = Config.put Metis_Tactic.verbose false ctxt in
       Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
         (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
     end
-  | Meson_Method => Meson_Tactic.meson_general_tac (silence_methods ctxt) global_facts
-  | SMT_Method =>
-    let val ctxt = Config.put SMT_Config.verbose false ctxt in
-      SMT_Solver.smt_tac ctxt global_facts
-    end
-  | Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts)
+  | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
+  | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+  | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
   | Simp_Size_Method =>
-    Simplifier.asm_full_simp_tac
-      (silence_methods ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
+    Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
   | _ =>
     Method.insert_tac global_facts THEN'
     (case meth of
       SATx_Method => SAT.satx_tac ctxt
     | Blast_Method => blast_tac ctxt
-    | Auto_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
-    | Force_Method => Clasimp.force_tac (silence_methods ctxt)
-    | Skolemize_method => skolem_tac (silence_methods ctxt)
+    | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
+    | Force_Method => Clasimp.force_tac ctxt
+    | Skolem_Method => skolem_tac ctxt
     | Linarith_Method =>
       let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
     | Presburger_Method => Cooper.tac true [] [] ctxt
     | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
 val simp_based_methods = [Simp_Method, Simp_Size_Method, Auto_Method, Force_Method, Skolem_Method]
 
 fun thms_influence_proof_method ctxt meth ths =
   not (member (op =) simp_based_methods meth) orelse
-  let val ctxt' = silence_methods ctxt in
-    (* unfortunate pointer comparison -- but it's always safe to consider a theorem useful *)
-    not (pointer_eq (ctxt' addsimps ths, ctxt'))
-  end
+  (* unfortunate pointer comparison -- but it's always safe to consider a theorem useful *)
+  not (pointer_eq (ctxt addsimps ths, ctxt))
 
 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
   | string_of_play_outcome (Play_Timed_Out time) =
     if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"
   | string_of_play_outcome Play_Failed = "failed"