src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 40554 ff446d5e9a62
parent 40526 ca3c6b1bfcdb
child 40627 becf5d5187cc
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Nov 15 18:56:29 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Nov 15 18:56:30 2010 +0100
     1.3 @@ -350,7 +350,8 @@
     1.4                   #> Config.put Sledgehammer.measure_run_time true)
     1.5      val params as {full_types, relevance_thresholds, max_relevant, ...} =
     1.6        Sledgehammer_Isar.default_params ctxt
     1.7 -          [("timeout", Int.toString timeout)]
     1.8 +          [("verbose", "true"),
     1.9 +           ("timeout", Int.toString timeout)]
    1.10      val default_max_relevant =
    1.11        Sledgehammer.default_max_relevant_for_prover thy prover_name
    1.12      val is_built_in_const =
    1.13 @@ -446,7 +447,9 @@
    1.14        |> Option.map (fst o read_int o explode)
    1.15        |> the_default 5
    1.16      val params = Sledgehammer_Isar.default_params ctxt
    1.17 -      [("provers", prover_name), ("timeout", Int.toString timeout)]
    1.18 +      [("verbose", "true"),
    1.19 +       ("provers", prover_name),
    1.20 +       ("timeout", Int.toString timeout)]
    1.21      val minimize =
    1.22        Sledgehammer_Minimize.minimize_facts params 1
    1.23                                             (Sledgehammer_Util.subgoal_count st)