# HG changeset patch
# User blanchet
# Date 1391085508 -3600
# Node ID b7ca9f98faca7f33b77e88f2abf1f6ca16d4cf19
# Parent  d187a9908e8480fe5f5970adc87f7f11e84cb3e4
made 'try0' (more) silent

diff -r d187a9908e84 -r b7ca9f98faca src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Jan 30 13:38:28 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Jan 30 13:38:28 2014 +0100
@@ -60,14 +60,7 @@
 (* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
    bound exceeded" warnings and the like. *)
 fun silence_reconstructors debug =
-  Config.put Metis_Tactic.verbose debug
+  Try0.silence_method debug
   #> Config.put SMT_Config.verbose debug
-  #> Config.put Lin_Arith.verbose debug
-  #> (not debug ?
-    (Context_Position.set_visible false
-     #> Proof_Context.background_theory (fn thy =>
-       thy
-       |> Context_Position.set_visible_global false
-       |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound))))
 
 end;
diff -r d187a9908e84 -r b7ca9f98faca src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Jan 30 13:38:28 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Thu Jan 30 13:38:28 2014 +0100
@@ -8,6 +8,8 @@
 sig
   val try0N : string
   val noneN : string
+
+  val silence_methods : bool -> Proof.context -> Proof.context
   val try0 :
     Time.time option -> string list * string list * string list * string list
     -> Proof.state -> bool
@@ -106,10 +108,21 @@
 fun time_string ms = string_of_int ms ^ " ms"
 fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms
 
+(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
+   bound exceeded" warnings and the like. *)
+fun silence_methods debug =
+  Config.put Metis_Tactic.verbose debug
+  #> Config.put Lin_Arith.verbose debug
+  #> (not debug ?
+    (Context_Position.set_visible false
+     #> Proof_Context.background_theory (fn thy =>
+       thy
+       |> Context_Position.set_visible_global false
+       |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound))))
+
 fun do_try0 mode timeout_opt quad st =
   let
-    val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
-      Config.put Lin_Arith.verbose false)
+    val st = st |> Proof.map_context (silence_methods false)
     fun trd (_, _, t) = t
     fun par_map f =
       if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself trd)