src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
changeset 72915 e05b77e1ab21
parent 72659 f8d25850173b
child 72924 590608c05386
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Nov 26 18:06:36 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Nov 26 18:45:19 2020 +0100
@@ -296,7 +296,7 @@
        val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS
        val (format, enc) =
          if modern then
-           (THF (With_FOOL, Monomorphic, THF_Lambda_Bool_Free), "mono_native_higher")
+           (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher")
          else
            (TFF (Without_FOOL, Monomorphic), "mono_native")
      in