# HG changeset patch
# User blanchet
# Date 1337865113 -7200
# Node ID 22846a7cf66ee655d278449b04044b88b18a0d80
# Parent  a1a5bf806d8bc28905f4d9c1735a213c1f98551f
update Satallax setup based on evaluation

diff -r a1a5bf806d8b -r 22846a7cf66e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 24 15:03:06 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 24 15:11:53 2012 +0200
@@ -366,7 +366,7 @@
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (true, ((120, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))],
+     K [(1.0, (true, ((60, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))],
    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}