# HG changeset patch
# User blanchet
# Date 1305274243 -7200
# Node ID 7b14bafe6778c7e6672a1c0e249dab4001c0c40a
# Parent  896aaab98563baa61851ac1fd9d0cbc600b5c5a5
tweak E slices

diff -r 896aaab98563 -r 7b14bafe6778 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri May 13 10:10:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri May 13 10:10:43 2011 +0200
@@ -222,7 +222,7 @@
      (* FUDGE *)
      if effective_e_weight_method ctxt = e_slicesN then
        [(0.333, (true, (100, ["mangled_preds?"]))) (* sym_offset_weight *),
-        (0.333, (true, (1000, ["mangled_preds?"]))) (* auto *),
+        (0.333, (true, (800, ["poly_tags!"]))) (* auto *),
         (0.334, (true, (200, ["mangled_preds?"]))) (* fun_weight *)]
      else
        [(1.0, (true, (250, ["mangled_preds?"])))]}