# HG changeset patch
# User blanchet
# Date 1367569644 -7200
# Node ID 3f2eacb8235a85b1c1d50f0762010f29f1a104df
# Parent  af2e0b2c4d7efea20eaaf86f3b4c69595700d072
tuning

diff -r af2e0b2c4d7e -r 3f2eacb8235a src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri May 03 10:26:34 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri May 03 10:27:24 2013 +0200
@@ -226,8 +226,8 @@
 
 (* E *)
 
-fun is_e_at_least_1_3 () = (string_ord (getenv "E_VERSION", "1.3") <> LESS)
-fun is_e_at_least_1_6 () = (string_ord (getenv "E_VERSION", "1.6") <> LESS)
+fun is_e_at_least_1_3 () = string_ord (getenv "E_VERSION", "1.3") <> LESS
+fun is_e_at_least_1_6 () = string_ord (getenv "E_VERSION", "1.6") <> LESS
 
 val tstp_proof_delims =
   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
@@ -530,10 +530,8 @@
 
 (* Vampire 1.8 has TFF support, but the support was buggy until revision
    1435 (or shortly before). *)
-fun is_vampire_at_least_1_8 () =
-  string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
-fun is_vampire_beyond_1_8 () =
-  string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
+fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
+fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
 
 val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)