# HG changeset patch
# User blanchet
# Date 1572013102 -7200
# Node ID d4ef7617e31e746fd8ca70dbb485fa76d29a74c7
# Parent  ce3a05ad07b7f2d3d6d958109829385a33fa8d37
repaired remote_vampire's proof reconstruction

diff -r ce3a05ad07b7 -r d4ef7617e31e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 15:59:25 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 16:18:22 2019 +0200
@@ -505,12 +505,10 @@
 
 val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS"
 
-(* cf. p. 20 of https://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
 val vampire_full_proof_options =
-  " --forced_options splitting=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:\
-  \naming=0"
+  " --forced_options equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
 
-val remote_vampire_full_proof_command =
+val remote_vampire_command =
   "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"
 
 val vampire_config : atp_config =
@@ -642,9 +640,8 @@
 
 fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice =
   {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
-   arguments = fn _ => fn full_proofs => fn full_proof_command => fn timeout => fn file_name => fn _ =>
-     (if full_proofs andalso full_proof_command <> "" then "-c " ^ quote full_proof_command ^ " "
-      else "") ^
+   arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
+     (if command <> "" then "-c " ^ quote command ^ " " else "") ^
      "-s " ^ the_remote_system system_name system_versions ^ " " ^
      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
      " " ^ file_name,
@@ -698,7 +695,7 @@
     (K (((100, ""), TFF Monomorphic, "mono_native", liftingN, false), "") (* FUDGE *))
 val remote_vampire =
   remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
-    (K (((400, ""), TFF Monomorphic, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
+    (K (((400, ""), TFF Monomorphic, "mono_native", combs_or_liftingN, false), remote_vampire_command) (* FUDGE *))
 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
 val remote_zipperposition =
   remotify_atp zipperposition "Zipperpin" ["1.5"]