diff -r 9ce354a77908 -r cbc398fb30bb src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 02 12:42:05 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 02 12:51:03 2012 +0100
@@ -363,11 +363,10 @@
    prem_kind = #prem_kind spass_config,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN,
-                       spass_incompleteN))),
-      (0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN,
-                       ""))),
-      (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN, "")))]}
+     [(0.334, (true, (300, DFG DFG_Sorted, "mono_simple", combsN,
+                      "" (* spass_incompleteN *)))),
+      (0.333, (true, (50, DFG DFG_Sorted, "mono_simple", combsN, ""))),
+      (0.333, (true, (150, DFG DFG_Sorted, "mono_simple", liftingN, "")))]}
 
 val spass_new = (spass_newN, spass_new_config)