--- 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, ...} =>
--- 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
--- 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;