# HG changeset patch
# User blanchet
# Date 1630067336 -7200
# Node ID 9c6159cbf9ee4d7ad86035d2af16df2e1197a22e
# Parent  5f0f0553762fd70c4747e289f1528ede32bd2540
disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax

diff -r 5f0f0553762f -r 9c6159cbf9ee src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Aug 26 23:23:16 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Aug 27 14:28:56 2021 +0200
@@ -550,7 +550,7 @@
 
 val zipperposition_config : atp_config =
   let
-    val format = THF (With_FOOL, Polymorphic, THF_Without_Choice)
+    val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice)
   in
     {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
      arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => fn _ =>
@@ -561,9 +561,9 @@
      prem_role = Hypothesis,
      best_slices = fn _ =>
        (* FUDGE *)
-       [(0.333, (((128, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_blsimp)),
-        (0.333, (((32, "meshN"), format, "poly_native_higher_fool", keep_lamsN, false), zipperposition_s6)),
-        (0.334, (((512, "meshN"), format, "mono_native_higher_fool", keep_lamsN, false), zipperposition_cdots))],
+       [(0.333, (((128, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
+        (0.333, (((32, "meshN"), format, "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
+        (0.334, (((512, "meshN"), format, "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}
   end