1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -372,10 +372,16 @@
     1.4          |> K ()
     1.5        end
     1.6      else if subcommand = minN then
     1.7 -      run_minimize (get_params Minimize ctxt
     1.8 -                               (("provers", [default_minimize_prover]) ::
     1.9 -                                override_params))
    1.10 -                   (K ()) (the_default 1 opt_i) (#add fact_override) state
    1.11 +      let
    1.12 +        val i = the_default 1 opt_i
    1.13 +        val params as {provers, ...} =
    1.14 +          get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
    1.15 +                                    override_params)
    1.16 +        val goal = prop_of (#goal (Proof.goal state))
    1.17 +        val facts = nearly_all_facts ctxt false fact_override Symtab.empty
    1.18 +                                     Termtab.empty [] [] goal
    1.19 +        val do_learn = mash_learn_proof ctxt params (hd provers) goal facts
    1.20 +      in run_minimize params do_learn i (#add fact_override) state end
    1.21      else if subcommand = messagesN then
    1.22        messages opt_i
    1.23      else if subcommand = supported_proversN then
    1.24 @@ -389,7 +395,7 @@
    1.25      else if subcommand = learnN orelse subcommand = relearnN then
    1.26        (if subcommand = relearnN then mash_unlearn ctxt else ();
    1.27         mash_learn ctxt (get_params Normal ctxt
    1.28 -                                   (("verbose", ["true"]) :: override_params)))
    1.29 +                                   (override_params @ [("verbose", ["true"])])))
    1.30      else if subcommand = kill_learnersN then
    1.31        kill_learners ()
    1.32      else if subcommand = running_learnersN then