src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML

            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN)
      in
        (* FUDGE *)
        K [((512, meshN), (format, type_enc, lam_trans, false, e_fun_weightN)),
         ((1024, meshN), (format, type_enc, lam_trans, false, e_sym_offset_weightN)),
-        ((91, mepoN), (format, type_enc, lam_trans, false, e_autoN)),
-        ((1000, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)),
+        ((128, mepoN), (format, type_enc, lam_trans, false, e_autoN)),
+        ((724, meshN), (format, "poly_guards??", lam_trans, false, e_sym_offset_weightN)),
         ((256, mepoN), (format, type_enc, liftingN, false, e_fun_weightN)),
         ((64, mashN), (format, type_enc, combsN, false, e_fun_weightN))]
      end,
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = default_max_new_mono_instances}