# HG changeset patch
# User desharna
# Date 1639865828 -3600
# Node ID 74c53a9027e291d11387a6ce4802eb24b35a9ea3
# Parent  aade20a03edb817fa9dc127f99efa6e681c21aaf
used TH1 for Leo-III in sledgehammer

diff -r aade20a03edb -r 74c53a9027e2 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Dec 18 23:11:49 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Dec 18 23:17:08 2021 +0100
@@ -384,7 +384,7 @@
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (((150, ""), THF (Polymorphic, {with_ite = true, with_let = true}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+     K [(1.0, (((512, ""), TH1, "mono_native_higher", keep_lamsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    best_max_new_mono_instances = default_max_new_mono_instances}