Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
authorblanchet
Mon, 30 May 2011 17:00:38 +0200
changeset 43060 e998e85e41ff
parent 43059 95b845a0edce
child 43061 8096eec997a9
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
src/HOL/Tools/ATP/atp_systems.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle