# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID 53b9326196fed904a0e61b4fb68eb33e0118fe74
# Parent  abec1d118bc9339706cda118c8a12d0def2f5788
don't be so verbose about SMT solver failures

diff -r abec1d118bc9 -r 53b9326196fe src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Sep 10 14:02:49 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -1122,7 +1122,7 @@
               (if show_filter then " " ^ quote fact_filter else "") ^
               " fact" ^ plural_s num_facts
             val _ =
-              if verbose andalso is_some outcome then
+              if debug then
                 quote name ^ " invoked with " ^
                 num_of_facts fact_filter num_facts ^ ": " ^
                 string_of_failure (failure_of_smt_failure (the outcome)) ^