# HG changeset patch
# User blanchet
# Date 1304681699 -7200
# Node ID b6a18a14cc5c735b793711056324ddae38e572d2
# Parent  42d607a9ae6557941712b047b94c2ec21fbd40be
better type system setup, based on Judgment Day

diff -r 42d607a9ae65 -r b6a18a14cc5c src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri May 06 11:57:21 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri May 06 13:34:59 2011 +0200
@@ -210,8 +210,10 @@
         (0.33334, (true, 200 (* FUDGE *))) (* fun_weight *)]
      else
        [(1.0, (true, 250 (* FUDGE *)))],
-   best_type_systems =
-     [ "args", "mangled_preds!", "mangled_preds?", "mangled_preds"]}
+   (* Actual order, according to Judgment Day: "mangled_preds!",
+      "mangled_tags!", "mangled_tags?", "mangled_preds?". But E "mangled_preds?"
+      works well in combination with Vampire "mangled_tags!". *)
+   best_type_systems = ["mangled_preds?"]}
 
 val e = (eN, e_config)
 
@@ -243,7 +245,7 @@
      K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
         (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
    best_type_systems =
-     ["mangled_preds!", "mangled_preds?", "args", "mangled_preds"]}
+     ["args", "mangled_preds!", "mangled_tags!", "mangled_tags?"]}
 
 val spass = (spassN, spass_config)
 
@@ -280,7 +282,7 @@
      K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
         (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
    best_type_systems =
-     ["mangled_preds?", "mangled_preds!", "args", "mangled_preds"]}
+     ["mangled_tags!", "mangled_preds!", "mangled_preds?"]}
 
 val vampire = (vampireN, vampire_config)