# HG changeset patch
# User blanchet
# Date 1572013616 -7200
# Node ID 718255bde391ffb493f72a008073d7b0ee085d0a
# Parent  d4ef7617e31e746fd8ca70dbb485fa76d29a74c7
invoke remote Vampire with higher-order (THF) syntax

diff -r d4ef7617e31e -r 718255bde391 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 16:18:22 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 16:26:56 2019 +0200
@@ -620,9 +620,9 @@
     | res => res
 
 fun get_remote_system name versions =
-  Synchronized.change_result remote_systems
-      (fn systems => (if null systems then get_remote_systems () else systems)
-                     |> `(`(find_remote_system name versions)))
+  Synchronized.change_result remote_systems (fn systems =>
+    (if null systems then get_remote_systems () else systems)
+    |> `(`(find_remote_system name versions)))
 
 fun the_remote_system name versions =
   (case get_remote_system name versions of
@@ -694,8 +694,8 @@
     [("refutation.", "end_refutation.")] [] Hypothesis
     (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_command) (* FUDGE *))
+  remotify_atp vampire "Vampire" ["THF-4.4"]
+    (K (((400, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *))
 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
 val remote_zipperposition =
   remotify_atp zipperposition "Zipperpin" ["1.5"]