src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

       (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then
          mash_unlearn ctxt (get_params Normal ctxt override_params)
        else
          ();
        mash_learn ctxt
+           (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
            (get_params Normal ctxt
                 ([("timeout",
                    [string_of_real default_learn_prover_timeout]),
                   ("slice", ["false"])] @
                  override_params @