src/HOL/Tools/ATP/atp_systems.ML

--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 05 08:03:28 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 05 09:43:39 2011 +0200
@@ -210,7 +210,8 @@
         (0.33334, (true, 200 (* FUDGE *))) (* fun_weight *)]
      else
        [(1.0, (true, 250 (* FUDGE *)))],
-   best_type_systems = ["args", "mangled_preds"]}
+   best_type_systems =
+     [ "args", "mangled_preds!", "mangled_preds?", "mangled_preds"]}
 
 val e = (eN, e_config)
 
@@ -241,7 +242,8 @@
    best_slices =
      K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
         (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
-   best_type_systems = ["mangled_preds"]}
+   best_type_systems =
+     ["mangled_preds!", "mangled_preds?", "args", "mangled_preds"]}
 
 val spass = (spassN, spass_config)
 
@@ -277,7 +279,8 @@
    best_slices =
      K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
         (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
-   best_type_systems = ["mangled_preds"]}
+   best_type_systems =
+     ["mangled_preds?", "mangled_preds!", "args", "mangled_preds"]}
 
 val vampire = (vampireN, vampire_config)
 
@@ -299,7 +302,7 @@
    hypothesis_kind = Hypothesis,
    formats = [Fof],
    best_slices = K [(1.0, (false, 250 (* FUDGE *)))],
-   best_type_systems = []}
+   best_type_systems = [] (* FIXME *)}
 
 val z3_atp = (z3_atpN, z3_atp_config)
 
@@ -381,7 +384,7 @@
              Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"]
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *))
-                     (#best_type_systems e_config)
+                     ["args", "preds", "tags"]
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r024"]
              [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof]