diff -r b86e8cf3f464 -r ffa31bf5c662 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 15:26:45 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 16:09:45 2012 +0200
@@ -528,7 +528,7 @@
 val vampire = (vampireN, fn () => vampire_config)
 
 
-(* Z3 with TPTP syntax *)
+(* Z3 with TPTP syntax (half experimental, half legacy) *)
 
 val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
 
@@ -665,9 +665,6 @@
 val remote_vampire =
   remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
       (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
-val remote_z3_tptp =
-  remotify_atp z3_tptp "Z3" ["3.0"]
-      (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
       (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
@@ -728,7 +725,7 @@
   [alt_ergo, e, e_males, iprover, iprover_eq, leo2, satallax, spass, spass_poly,
    vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, remote_e_tofof,
    remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax,
-   remote_vampire, remote_z3_tptp, remote_snark, remote_waldmeister]
+   remote_vampire, remote_snark, remote_waldmeister]
 
 val setup = fold add_atp atps