# HG changeset patch
# User blanchet
# Date 1304338954 -7200
# Node ID ec29be07cd9dcc8f18965657846e0124510bae88
# Parent  def5846169ce2ecdfc4906a7d94ef3a6db3a481e
supply type-system defaults for major ATPs

diff -r def5846169ce -r ec29be07cd9d src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 02 14:21:57 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 02 14:22:34 2011 +0200
@@ -84,6 +84,9 @@
   Preds of polymorphism * type_level |
   Tags of polymorphism * type_level
 
+val mangled_preds = Preds (Mangled_Monomorphic, All_Types)
+val const_args = Preds (Polymorphic, Const_Arg_Types)
+
 fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic
   | polymorphism_of_type_sys (Preds (poly, _)) = poly
   | polymorphism_of_type_sys (Tags (poly, _)) = poly
@@ -237,7 +240,7 @@
         (0.33334, (true, 200 (* FUDGE *))) (* E_Fun_Weight *)]
      else
        [(1.0, (true, 250 (* FUDGE *)))],
-   best_type_systems = []}
+   best_type_systems = [const_args, mangled_preds]}
 
 val e = (eN, e_config)
 
@@ -268,7 +271,7 @@
    best_slices =
      K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
         (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
-   best_type_systems = []}
+   best_type_systems = [mangled_preds]}
 
 val spass = (spassN, spass_config)
 
@@ -304,7 +307,7 @@
    best_slices =
      K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
         (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
-   best_type_systems = []}
+   best_type_systems = [mangled_preds]}
 
 val vampire = (vampireN, vampire_config)
 
@@ -408,7 +411,7 @@
              Conjecture [Tff] (K 200 (* FUDGE *)) []
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *))
-                     []
+                     (#best_type_systems e_config)
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r024"]
              [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof]