# HG changeset patch
# User wenzelm
# Date 1736086710 -3600
# Node ID 6e25f82056ad82d6c8e3154be8840d05ec329a3b
# Parent  4ab59fef89eafab134998f26177d1e224f6a32c3
tuned (NB: string_ord is required here for its precedence on length);

diff -r 4ab59fef89ea -r 6e25f82056ad src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sun Jan 05 15:04:42 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sun Jan 05 15:18:30 2025 +0100
@@ -204,10 +204,10 @@
 
 val old_e_config : atp_config = make_e_config default_max_new_mono_instances (let
        val (format, type_enc, lam_trans, extra_options) =
-         if string_ord (getenv "E_VERSION", "3.0") <> LESS then
+         if is_greater_equal (string_ord (getenv "E_VERSION", "3.0")) then
            (* '$ite' support appears to be unsound. *)
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true")
-         else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
+         else if is_greater_equal (string_ord (getenv "E_VERSION", "2.6")) then
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule")
          else
            (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule")