1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Feb 02 10:13:14 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Feb 02 17:25:55 2013 +0100
     1.3 @@ -336,9 +336,12 @@
     1.4       let val heuristic = effective_e_selection_heuristic ctxt in
     1.5         (* FUDGE *)
     1.6         if heuristic = e_smartN then
     1.7 -         [(0.333, (((500, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
     1.8 -          (0.334, (((50, meshN), FOF, "mono_guards??", combsN, false), e_fun_weightN)),
     1.9 -          (0.333, (((1000, mepoN), FOF, "mono_tags??", combsN, false), e_sym_offset_weightN))]
    1.10 +         [(0.15, (((128, meshN), FOF, "mono_tags??", combsN, false), e_fun_weightN)),
    1.11 +          (0.15, (((128, mashN), FOF, "mono_guards??", combsN, false), e_sym_offset_weightN)),
    1.12 +          (0.15, (((91, mepoN), FOF, "mono_tags??", combsN, false), e_autoN)),
    1.13 +          (0.15, (((64, mashN), FOF, "mono_guards??", combsN, false), e_fun_weightN)),
    1.14 +          (0.15, (((1000, meshN), FOF, "poly_guards??", combsN, false), e_sym_offset_weightN)),
    1.15 +          (0.25, (((256, mepoN), FOF, "mono_tags??", liftingN, false), e_fun_weightN))]
    1.16         else
    1.17           [(1.0, (((500, ""), FOF, "mono_tags??", combsN, false), heuristic))]
    1.18       end,
    1.19 @@ -560,7 +563,7 @@
    1.20       (if is_vampire_beyond_1_8 () then
    1.21          [(0.333, (((500, meshN), vampire_tff0, "mono_guards??", combs_or_liftingN, false), sosN)),
    1.22           (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)),
    1.23 -         (0.334, (((50, mepoN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
    1.24 +         (0.334, (((50, meshN), vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
    1.25        else
    1.26          [(0.333, (((150, meshN), FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
    1.27           (0.333, (((500, meshN), FOF, "mono_tags??", combs_or_liftingN, false), sosN)),