# HG changeset patch
# User desharna
# Date 1743408948 -7200
# Node ID 7ed32d7f83175ce9078f0e20cf59fab34bf5c636
# Parent  41ae659861ef450f6b7ccf096b05e9b73c0052e3
removed old Vampire configuration from Sledgehammer

diff -r 41ae659861ef -r 7ed32d7f8317 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Mar 31 09:50:28 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Mar 31 10:15:48 2025 +0200
@@ -384,13 +384,6 @@
 
 local
 
-val old_vampire_basic_options =
-  ["--proof tptp",
-   "--output_axiom_names on"] @
-  (if ML_System.platform_is_windows
-   then []  (*time slicing is not support in the Windows version of Vampire*)
-   else ["--mode casc"])
-
 val new_vampire_basic_options =
   ["--input_syntax tptp",
    "--proof tptp",
@@ -428,19 +421,7 @@
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = good_max_new_mono_instances}
 
-val old_vampire_config : atp_config =
-  (* FUDGE *)
-  make_vampire_config old_vampire_basic_options (2 * default_max_new_mono_instances)
-  [((2, false, false, 512, meshN), (TX1, "mono_native", combsN, false, sosN)),
-   ((2, false, false, 1024, meshN), (TX1, "mono_native", liftingN, false, sosN)),
-   ((2, false, false, 256, mashN), (TX1, "mono_native", liftingN, false, no_sosN)),
-   ((2, false, true, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)),
-   ((2, false, false, 16, meshN), (TX1, "mono_native", liftingN, false, no_sosN)),
-   ((2, false, false, 32, meshN), (TX1, "mono_native", combsN, false, no_sosN)),
-   ((2, false, false, 64, meshN), (TX1, "mono_native", combs_or_liftingN, false, no_sosN)),
-   ((2, false, false, 128, meshN), (TX1, "mono_native", liftingN, false, no_sosN))]
-
-val new_vampire_config : atp_config =
+val vampire_config : atp_config =
   (* 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, ""))),
@@ -465,11 +446,7 @@
 
 in
 
-val vampire = (vampireN, fn () =>
-  if string_ord (getenv "VAMPIRE_VERSION", "4.8") <> LESS then
-    new_vampire_config
-  else
-    old_vampire_config)
+val vampire = (vampireN, fn () => vampire_config)
 
 end