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,6 +372,7 @@
     1.4        end
     1.5      else if subcommand = minN then
     1.6        let
     1.7 +        val ctxt = ctxt |> Config.put instantiate_inducts false
     1.8          val i = the_default 1 opt_i
     1.9          val params as {provers, ...} =
    1.10            get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
    1.11 @@ -403,8 +404,9 @@
    1.12                              override_params @
    1.13                              [("slice", ["false"]),
    1.14                               ("minimize", ["true"]),
    1.15 -                             ("preplay_timeout", ["0"])])))
    1.16 -           (subcommand = learn_atpN orelse subcommand = relearn_atpN)
    1.17 +                             ("preplay_timeout", ["0"])]))
    1.18 +                  fact_override (#facts (Proof.goal state))
    1.19 +                  (subcommand = learn_atpN orelse subcommand = relearn_atpN))
    1.20      else if subcommand = kill_learnersN then
    1.21        kill_learners ()
    1.22      else if subcommand = running_learnersN then