--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100
@@ -428,6 +428,7 @@
fun timed_reconstructor reconstr debug timeout ths =
(Config.put Metis_Tactic.verbose debug
+ #> Config.put SMT_Config.verbose debug
#> (fn ctxt => tac_for_reconstructor reconstr ctxt ths))
|> timed_apply timeout
@@ -869,6 +870,7 @@
val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
val repair_context =
select_smt_solver name
+ #> Config.put SMT_Config.verbose debug
#> (if overlord then
Config.put SMT_Config.debug_files
(overlord_file_location_for_prover name