# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID e998e85e41ff3f858521cdc188c70a7d1815184a
# Parent  95b845a0edce749be2c6f8ac680c3d29c524eea1
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples

diff -r 95b845a0edce -r e998e85e41ff src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 30 17:00:38 2011 +0200
@@ -221,8 +221,8 @@
    best_slices = fn ctxt =>
      (* FUDGE *)
      if effective_e_weight_method ctxt = e_slicesN then
-       [(0.333, (true, (100, ["poly_preds"]))) (* sym_offset_weight *),
-        (0.333, (true, (800, ["mangled_preds_heavy"]))) (* auto *),
+       [(0.333, (true, (100, ["mangled_preds_heavy"]))) (* sym_offset_weight *),
+        (0.333, (true, (800, ["poly_preds?"]))) (* auto *),
         (0.334, (true, (200, ["mangled_tags!", "mangled_tags?"])))
                                                                (* fun_weight *)]
      else