src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

       st |> Proof.map_context
                 (change_dir dir
                  #> Config.put Sledgehammer.measure_run_time true)
     val params as {full_types, relevance_thresholds, max_relevant, ...} =
       Sledgehammer_Isar.default_params ctxt
-          [("timeout", Int.toString timeout)]
+          [("verbose", "true"),
+           ("timeout", Int.toString timeout)]
     val default_max_relevant =
       Sledgehammer.default_max_relevant_for_prover thy prover_name
     val is_built_in_const =
       Sledgehammer.is_built_in_const_for_prover ctxt prover_name
     val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name

     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o explode)
       |> the_default 5
     val params = Sledgehammer_Isar.default_params ctxt
-      [("provers", prover_name), ("timeout", Int.toString timeout)]
+      [("verbose", "true"),
+       ("provers", prover_name),
+       ("timeout", Int.toString timeout)]
     val minimize =
       Sledgehammer_Minimize.minimize_facts params 1
                                            (Sledgehammer_Util.subgoal_count st)
     val _ = log separator
   in