# HG changeset patch
# User blanchet
# Date 1344950608 -7200
# Node ID 55874425fd32701583fd29618ac3f0f893b55074
# Parent  943bb96b4e129ea0cd6a313a66983e127d6ded49
tweak Vampire setup in the light of new evaluation

diff -r 943bb96b4e12 -r 55874425fd32 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 15:18:11 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 14 15:23:28 2012 +0200
@@ -513,8 +513,8 @@
    best_slices = fn ctxt =>
      (* FUDGE *)
      (if is_vampire_beyond_1_8 () then
-        [(0.333, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
-         (0.333, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN)),
+        [(0.333, ((500, vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
+         (0.333, ((150, vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
          (0.334, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
       else
         [(0.333, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN)),