src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

             fun num_of_facts fact_filter num_facts =
               string_of_int num_facts ^
               (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)) ^
                 " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
                 "..."