--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:46 2012 +0200
@@ -372,6 +372,7 @@
end
else if subcommand = minN then
let
+ val ctxt = ctxt |> Config.put instantiate_inducts false
val i = the_default 1 opt_i
val params as {provers, ...} =
get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
@@ -403,8 +404,9 @@
override_params @
[("slice", ["false"]),
("minimize", ["true"]),
- ("preplay_timeout", ["0"])])))
- (subcommand = learn_atpN orelse subcommand = relearn_atpN)
+ ("preplay_timeout", ["0"])]))
+ fact_override (#facts (Proof.goal state))
+ (subcommand = learn_atpN orelse subcommand = relearn_atpN))
else if subcommand = kill_learnersN then
kill_learners ()
else if subcommand = running_learnersN then