# HG changeset patch
# User desharna
# Date 1632300402 -7200
# Node ID 398b7bb9ebdd030c3ddc273eb92c2de106c6a294
# Parent  f984d30cd0c3726367a714496d47ae2c90e3f792
used Vampire 4.5.1 in Sledgehammer

diff -r f984d30cd0c3 -r 398b7bb9ebdd src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Sep 21 20:56:28 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Sep 22 10:46:42 2021 +0200
@@ -319,7 +319,7 @@
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     ["--clausifier \"$OLD_VAMPIRE_HOME\"/vampire " ^
+     ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^
       "--clausifier_options \"--mode clausify\" " ^
       "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
@@ -490,7 +490,7 @@
   let
     val format = TFF (Without_FOOL, Monomorphic)
   in
-    {exec = (["OLD_VAMPIRE_HOME"], ["vampire"]),
+    {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
        (check_vampire_noncommercial ();
         [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^