# HG changeset patch
# User desharna
# Date 1613125092 -3600
# Node ID f6f1242ed3672872147725b36bdcea582a20624f
# Parent  3e963d68d394aca8ba91d3fa71ab9dae4c4bf07c
proper prover capabilities for zipperposition

diff -r 3e963d68d394 -r f6f1242ed367 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Feb 09 14:13:03 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Feb 12 11:18:12 2021 +0100
@@ -553,9 +553,9 @@
    prem_role = Conjecture,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(0.333, (((128, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
+     [(0.333, (((128, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
       (0.333, (((32, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
-      (0.334, (((512, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
+      (0.334, (((512, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}