# HG changeset patch
# User blanchet
# Date 1626166634 -7200
# Node ID 6a0e1c14a8c25cc29ed92888365ac6d65f992cfa
# Parent  f0d231ead66091e8f10281dda89f2e6dccac0ce2
wait for E 2.7 before using 'ite' in HO mode

diff -r f0d231ead660 -r 6a0e1c14a8c2 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Jul 13 10:57:14 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Jul 13 10:57:14 2021 +0200
@@ -290,10 +290,12 @@
      let
        val heuristic = Config.get ctxt e_selection_heuristic
        val (format, enc) =
-         if string_ord (getenv "E_VERSION", "2.6") <> LESS then
+         if string_ord (getenv "E_VERSION", "2.7") <> LESS then
            (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher_fool")
+         else if string_ord (getenv "E_VERSION", "2.6") <> LESS then
+           (THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher")
          else
-           (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher")
+           (THF (Without_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher")
      in
        (* FUDGE *)
        if heuristic = e_smartN then