# HG changeset patch
# User desharna
# Date 1709713600 -3600
# Node ID dd4e532a0d44060649a49a9c3655412f57b67505
# Parent  db72d9920186132e3e7252bd60a17c3fb0f060e7
removed unused variable

diff -r db72d9920186 -r dd4e532a0d44 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Mar 06 09:25:34 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Mar 06 09:26:40 2024 +0100
@@ -459,9 +459,8 @@
    ((2, false, false, 128, meshN), (TX1, "mono_native", liftingN, false, no_sosN))]
 
 val new_vampire_config : atp_config =
-  let val infinity = 1000 in
-    (* FUDGE: this solved 998/1500 (66.53 %) using MePo when testing *)
-    make_vampire_config new_vampire_basic_options 256
+  (* FUDGE: this solved 998/1500 (66.53 %) using MePo when testing *)
+  make_vampire_config new_vampire_basic_options 256
     [(((2, false, false,  512, meshN), (TX0, "mono_native_fool", liftingN, false, ""))),
      (((2, false, false, 2048, meshN), (TX0, "mono_native_fool", combsN, false, ""))),
      (((2, false, false,  128, meshN), (TX0, "mono_native_fool", liftingN, false, ""))),
@@ -481,7 +480,6 @@
      (((2, false, false,  512, meshN), (TH0_MINUS, "mono_native_higher", keep_lamsN, false, ""))),
      (((2, false, false,  512, meshN), (TX0, "mono_native_fool", combsN, false, ""))),
      (((2, false, false, 1024, meshN), (TX1, "poly_native_fool", combsN, false, "")))]
-  end
 
 in