# HG changeset patch
# User blanchet
# Date 1314110243 -7200
# Node ID 867928fe20e930b504fdac46ffe7bcfc076ab523
# Parent  2434dd7519e8bc938eb9ba767f77a839b3ca17c9
always use TFF if possible

diff -r 2434dd7519e8 -r 867928fe20e9 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 16:14:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 16:37:23 2011 +0200
@@ -334,12 +334,13 @@
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
-     (0.333, (false, (150, FOF, "poly_guards", sosN))) ::
      (if is_old_vampire_version () then
-        [(0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
+        [(0.333, (false, (150, FOF, "poly_guards", sosN))),
+         (0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
          (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
       else
-        [(0.334, (true, (50, TFF, "simple", no_sosN))),
+        [(0.333, (false, (150, TFF, "poly_guards", sosN))),
+         (0.334, (true, (50, TFF, "simple", no_sosN))),
          (0.333, (false, (500, TFF, "simple", sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}