# HG changeset patch
# User blanchet
# Date 1289843790 -3600
# Node ID ff446d5e9a62ba907f33272dacd85db180cfb399
# Parent  1264c91723386c23980e22d7b30a2e9e7f4231a7
turn on Sledgehammer verbosity so we can track down crashes

diff -r 1264c9172338 -r ff446d5e9a62 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Nov 15 18:56:29 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Nov 15 18:56:30 2010 +0100
@@ -350,7 +350,8 @@
                  #> 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 =
@@ -446,7 +447,9 @@
       |> 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)