# HG changeset patch
# User blanchet
# Date 1435098603 -7200
# Node ID 6a363e56ffff6b07fed9c0c59a0fe37d28b9f760
# Parent  b28677f33eaa7394367a54ad09622e99c89203f1
silence 'try'

diff -r b28677f33eaa -r 6a363e56ffff src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Jun 23 16:56:40 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jun 24 00:30:03 2015 +0200
@@ -292,6 +292,9 @@
 fun get_params mode = extract_params mode o default_raw_params mode
 fun default_params thy = get_params Normal thy o map (apsnd single)
 
+val silence_state =
+  Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false)
+
 (* Sledgehammer the given subgoal *)
 
 val default_learn_prover_timeout = 2.0
@@ -314,7 +317,7 @@
         end
     val state = state0
       |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained)
-      |> Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false)
+      |> silence_state
 
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -324,9 +327,8 @@
   in
     if subcommand = runN then
       let val i = the_default 1 opt_i in
-        ignore
-          (run_sledgehammer
-            (get_params Normal thy override_params) Normal output_result i fact_override state)
+        ignore (run_sledgehammer
+          (get_params Normal thy override_params) Normal output_result i fact_override state)
       end
     else if subcommand = messagesN then
       messages opt_i
@@ -400,7 +402,7 @@
     val mode = if auto then Auto_Try else Try
     val i = 1
   in
-    run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override state
+    run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state)
   end
 
 val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))