# HG changeset patch
# User blanchet
# Date 1400260430 -7200
# Node ID 51d4189d95cf357b47f2b34c72abcc7f2af6c3a9
# Parent  3ef45ce002b5139b3bf79e79eb255176e30a564d
silence methods even better

diff -r 3ef45ce002b5 -r 51d4189d95cf src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri May 16 19:13:50 2014 +0200
@@ -279,8 +279,7 @@
     val overlord = lookup_bool "overlord"
     val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
     val blocking =
-      Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
-      lookup_bool "blocking"
+      Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking"
     val provers = lookup_string "provers" |> space_explode " "
                   |> mode = Auto_Try ? single o hd
     val type_enc =
@@ -360,7 +359,8 @@
 
 fun hammer_away override_params subcommand opt_i fact_override state0 =
   let
-    val state = Proof.map_context (Try0.silence_methods false) state0
+    val state =
+      Proof.map_contexts (Try0.silence_methods false #> Config.put SMT2_Config.verbose false) state0
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 
diff -r 3ef45ce002b5 -r 51d4189d95cf src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri May 16 19:13:50 2014 +0200
+++ b/src/HOL/Tools/try0.ML	Fri May 16 19:13:50 2014 +0200
@@ -122,7 +122,7 @@
 
 fun generic_try0 mode timeout_opt quad st =
   let
-    val st = st |> Proof.map_context (silence_methods false);
+    val st = Proof.map_contexts (silence_methods false) st;
     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)