wait for E 2.7 before using 'ite' in HO mode
authorblanchet
Tue, 13 Jul 2021 10:57:14 +0200
changeset 73974 6a0e1c14a8c2
parent 73973 f0d231ead660
child 73975 8d93f9ca6518
wait for E 2.7 before using 'ite' in HO mode
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