src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

                          state
         |> K ()
       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]) ::
                                     override_params)
         val goal = prop_of (#goal (Proof.goal state))

                            (("timeout",
                              [string_of_real default_learn_atp_timeout]) ::
                             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
       running_learners ()
     else if subcommand = refresh_tptpN then