--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jan 31 15:39:45 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jan 31 16:11:15 2012 +0100
@@ -362,11 +362,11 @@
prem_kind = #prem_kind spass_config,
best_slices = fn _ =>
(* FUDGE *)
- [(0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN,
+ [(0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN,
""))),
- (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN,
+ (0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN,
spass_incompleteN))),
- (0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN,
+ (0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN,
"")))]}
val spass_new = (spass_newN, spass_new_config)