1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 02 12:42:05 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 02 12:51:03 2012 +0100
     1.3 @@ -363,11 +363,10 @@
     1.4     prem_kind = #prem_kind spass_config,
     1.5     best_slices = fn _ =>
     1.6       (* FUDGE *)
     1.7 -     [(0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN,
     1.8 -                       spass_incompleteN))),
     1.9 -      (0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN,
    1.10 -                       ""))),
    1.11 -      (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN, "")))]}
    1.12 +     [(0.334, (true, (300, DFG DFG_Sorted, "mono_simple", combsN,
    1.13 +                      "" (* spass_incompleteN *)))),
    1.14 +      (0.333, (true, (50, DFG DFG_Sorted, "mono_simple", combsN, ""))),
    1.15 +      (0.333, (true, (150, DFG DFG_Sorted, "mono_simple", liftingN, "")))]}
    1.16  
    1.17  val spass_new = (spass_newN, spass_new_config)
    1.18