# HG changeset patch
# User blanchet
# Date 1307396762 -7200
# Node ID 2c88166938eb2dbef040fb721ae4fe5dffba98ce
# Parent  a6bda1a47c0a1b511bfba6dab3843436d486c5f4
slighly more reasonable Vampire slices (until new monomorphizer is used)

diff -r a6bda1a47c0a -r 2c88166938eb src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 06 23:43:28 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 06 23:46:02 2011 +0200
@@ -302,8 +302,8 @@
    formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (400, ["mangled_preds_heavy"]))) (* SOS *),
-      (0.333, (false, (400, ["mangled_tags?"]))) (* SOS *),
+     [(0.333, (false, (200, ["mangled_preds_heavy"]))) (* SOS *),
+      (0.333, (false, (300, ["mangled_tags?"]))) (* SOS *),
       (0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)]
      |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
          else I)}