# HG changeset patch
# User blanchet
# Date 1308559262 -7200
# Node ID 1cef683b588bc2401512b327ce46b7f8cb1e88c0
# Parent  b0cf8f9bd1924b584ecb2d081400aae26cd56ea1
slightly better setup for E

diff -r b0cf8f9bd192 -r 1cef683b588b src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 10:41:02 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jun 20 10:41:02 2011 +0200
@@ -155,7 +155,7 @@
 fun e_weight_method_case method fw sow =
   if method = e_fun_weightN then fw
   else if method = e_sym_offset_weightN then sow
-  else raise Fail ("unexpected" ^ quote method)
+  else raise Fail ("unexpected " ^ quote method)
 
 fun scaled_e_weight ctxt method w =
   w * Config.get ctxt
@@ -214,9 +214,9 @@
      let val method = effective_e_weight_method ctxt in
        (* FUDGE *)
        if method = e_smartN then
-         [(0.333, (true, (200, ["mangled_preds"], e_sym_offset_weightN))),
-          (0.333, (true, (1000, ["mangled_preds?"], e_fun_weightN))),
-          (0.334, (true, (50, ["mangled_tags?"], e_sym_offset_weightN)))]
+         [(0.333, (true, (500, ["mangled_tags?"], e_fun_weightN))),
+          (0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN))),
+          (0.334, (true, (50, ["mangled_preds?"], e_fun_weightN)))]
        else
          [(1.0, (true, (300, ["mangled_tags?"], method)))]
      end}