diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -34,11 +34,11 @@
     (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
 
   val string_of_proof_method : proof_method -> string
-  val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
+  val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int ->
+    tactic
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome * play_outcome -> order
   val one_line_proof_text : int -> one_line_params -> string
-  val silence_proof_methods : bool -> Proof.context -> Proof.context
 end;
 
 structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
@@ -89,27 +89,36 @@
   | Presburger_Method => "presburger"
   | Algebra_Method => "algebra")
 
-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) =>
-    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
-  | Meson_Method => Meson.meson_tac ctxt global_facts
-  | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
-  | _ =>
-    Method.insert_tac global_facts THEN'
+(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
+   exceeded" warnings and the like. *)
+fun silence_proof_methods debug =
+  Try0.silence_methods debug
+  #> Config.put SMT_Config.verbose debug
+
+fun tac_of_proof_method ctxt0 debug (local_facts, global_facts) meth =
+  let val ctxt = silence_proof_methods debug ctxt0 in
+    Method.insert_tac local_facts THEN'
     (case meth of
-      Blast_Method => blast_tac ctxt
-    | Simp_Method => Simplifier.asm_full_simp_tac ctxt
-    | Simp_Size_Method =>
-      Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
-    | Auto_Method => K (Clasimp.auto_tac ctxt)
-    | Fastforce_Method => Clasimp.fast_force_tac ctxt
-    | Force_Method => Clasimp.force_tac ctxt
-    | Linarith_Method => Lin_Arith.tac ctxt
-    | Presburger_Method => Cooper.tac true [] [] ctxt
-    | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+      Metis_Method (type_enc_opt, lam_trans_opt) =>
+      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
+    | Meson_Method => Meson.meson_tac ctxt global_facts
+
+    | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+    | _ =>
+      Method.insert_tac global_facts THEN'
+      (case meth of
+        Blast_Method => blast_tac ctxt
+      | Simp_Method => Simplifier.asm_full_simp_tac ctxt
+      | Simp_Size_Method =>
+        Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
+      | Auto_Method => K (Clasimp.auto_tac ctxt)
+      | Fastforce_Method => Clasimp.fast_force_tac ctxt
+      | Force_Method => Clasimp.force_tac ctxt
+      | Linarith_Method => Lin_Arith.tac ctxt
+      | Presburger_Method => Cooper.tac true [] [] ctxt
+      | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+  end
 
 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
   | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
@@ -189,10 +198,4 @@
     try_line ^ minimize_line minimize_command (map fst (extra @ chained))
   end
 
-(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
-   exceeded" warnings and the like. *)
-fun silence_proof_methods debug =
-  Try0.silence_methods debug
-  #> Config.put SMT_Config.verbose debug
-
 end;