diff -r 646651bcf261 -r fe114eca312e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 15:05:03 2019 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 25 15:18:06 2019 +0200
@@ -712,6 +712,9 @@
 val remote_agsyhol =
   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
     (K (((60, ""), THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
+val remote_alt_ergo =
+  remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"]
+    (K (((250, ""), TFF Polymorphic, "poly_native", keep_lamsN, false), "") (* FUDGE *))
 val remote_e =
   remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
     (K (((750, ""), TFF Monomorphic, "mono_native", combsN, false), "") (* FUDGE *))
@@ -724,13 +727,13 @@
 val remote_leo3 =
   remotify_atp leo3 "Leo-III" ["1.1"]
     (K (((150, ""), THF (Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, 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 *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"]
     [("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_full_proof_command) (* FUDGE *))
 val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??"
 
 
@@ -768,8 +771,8 @@
 
 val atps =
   [agsyhol, alt_ergo, e, e_males, e_par, ehoh, iprover, leo2, leo3, satallax, spass, vampire,
-   z3_tptp, zipperposition, remote_agsyhol, remote_e, remote_iprover, remote_leo2, remote_leo3,
-   remote_vampire, remote_snark, remote_pirate, remote_waldmeister]
+   z3_tptp, zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover,
+   remote_leo2, remote_leo3, remote_vampire, remote_snark, remote_pirate, remote_waldmeister]
 
 val _ = Theory.setup (fold add_atp atps)