# HG changeset patch
# User blanchet
# Date 1391039952 -3600
# Node ID cdb9435e3caed0512c099dea181c364274d955b0
# Parent  fda77499eef5f5a9a64b5917e4b3961ed2af4533
silenced reconstructors in Sledgehammer

diff -r fda77499eef5 -r cdb9435e3cae src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Wed Jan 29 23:24:34 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 30 00:59:12 2014 +0100
@@ -131,9 +131,7 @@
           end)
 
       val facts = map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
-
-      val ctxt' = ctxt
-        |> debug ? (Config.put Metis_Tactic.verbose true #> Config.put Lin_Arith.verbose true)
+      val ctxt' = ctxt |> silence_reconstructors debug
 
       fun prove () =
         Goal.prove ctxt' [] [] goal (fn {context = ctxt, ...} =>
diff -r fda77499eef5 -r cdb9435e3cae src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jan 29 23:24:34 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 30 00:59:12 2014 +0100
@@ -381,10 +381,8 @@
   | tac_of_reconstructor SMT = SMT_Solver.smt_tac
 
 fun timed_reconstructor reconstr debug timeout ths =
-  (Config.put Metis_Tactic.verbose debug
-   #> Config.put SMT_Config.verbose debug
-   #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
-  |> timed_apply timeout
+  timed_apply timeout (silence_reconstructors debug
+    #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
 
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 
diff -r fda77499eef5 -r cdb9435e3cae src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Wed Jan 29 23:24:34 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Jan 30 00:59:12 2014 +0100
@@ -26,6 +26,8 @@
     (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
 
   val smtN : string
+
+  val silence_reconstructors : bool -> Proof.context -> Proof.context
 end;
 
 structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
@@ -55,4 +57,17 @@
 
 val smtN = "smt"
 
+(* 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
+  #> 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;