get rid of remote_vampire since it's hard, if possible at all, to follow Vampire's online options

--- a/src/Doc/Sledgehammer/document/root.tex	Thu Jul 15 22:51:49 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Fri Jul 16 15:27:55 2021 +0200
@@ -803,9 +803,6 @@
 \item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
-Vampire runs on Geoff Sutcliffe's Miami servers.
-
 \item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
 equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
 used to prove universally quantified equations using unconditional equations,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Jul 15 22:51:49 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Jul 16 15:27:55 2021 +0200
@@ -482,9 +482,6 @@
 val vampire_full_proof_options =
   " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
 
-val remote_vampire_command =
-  "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"
-
 val vampire_config : atp_config =
   let
     val format = TFF (Without_FOOL, Monomorphic)
@@ -663,9 +660,6 @@
 val remote_leo3 =
   remotify_atp leo3 "Leo-III" ["1.1"]
     (K (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
-val remote_vampire =
-  remotify_atp vampire "Vampire" ["THF-4.4"]
-    (K (((400, ""), THF (Without_FOOL, 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" ["2.0"]
@@ -728,7 +722,7 @@
 val atps =
   [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
    remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
-   remote_vampire, remote_waldmeister, remote_zipperposition, dummy_tfx]
+   remote_waldmeister, remote_zipperposition, dummy_tfx]
 
 val _ = Theory.setup (fold add_atp atps)