1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 13 09:58:08 2013 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 13 10:26:56 2013 +0200
     1.3 @@ -211,8 +211,7 @@
     1.4  
     1.5  (* agsyHOL *)
     1.6  
     1.7 -val agsyhol_thf0 =
     1.8 -  THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
     1.9 +val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
    1.10  
    1.11  val agsyhol_config : atp_config =
    1.12    {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
    1.13 @@ -233,7 +232,7 @@
    1.14  
    1.15  (* Alt-Ergo *)
    1.16  
    1.17 -val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
    1.18 +val alt_ergo_tff1 = TFF Polymorphic
    1.19  
    1.20  val alt_ergo_config : atp_config =
    1.21    {exec = K (["WHY3_HOME"], ["why3"]),
    1.22 @@ -462,8 +461,7 @@
    1.23  
    1.24  (* LEO-II supports definitions, but it performs significantly better on our
    1.25     benchmarks when they are not used. *)
    1.26 -val leo2_thf0 =
    1.27 -  THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
    1.28 +val leo2_thf0 = THF (Monomorphic, THF_Without_Choice, THF_Without_Defs)
    1.29  
    1.30  val leo2_config : atp_config =
    1.31    {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
    1.32 @@ -490,8 +488,7 @@
    1.33  (* Satallax *)
    1.34  
    1.35  (* Choice is disabled until there is proper reconstruction for it. *)
    1.36 -val satallax_thf0 =
    1.37 -  THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
    1.38 +val satallax_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
    1.39  
    1.40  val satallax_config : atp_config =
    1.41    {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
    1.42 @@ -568,7 +565,7 @@
    1.43  fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
    1.44  fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
    1.45  
    1.46 -val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
    1.47 +val vampire_tff0 = TFF Monomorphic
    1.48  
    1.49  val vampire_config : atp_config =
    1.50    {exec = K (["VAMPIRE_HOME"], ["vampire"]),
    1.51 @@ -620,7 +617,7 @@
    1.52  
    1.53  (* Z3 with TPTP syntax (half experimental, half legacy) *)
    1.54  
    1.55 -val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
    1.56 +val z3_tff0 = TFF Monomorphic
    1.57  
    1.58  val z3_tptp_config : atp_config =
    1.59    {exec = K (["Z3_HOME"], ["z3"]),
    1.60 @@ -657,8 +654,7 @@
    1.61     best_max_mono_iters = default_max_mono_iters,
    1.62     best_max_new_mono_instances = default_max_new_mono_instances}
    1.63  
    1.64 -val dummy_thf_format =
    1.65 -  THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
    1.66 +val dummy_thf_format = THF (Polymorphic, THF_With_Choice, THF_With_Defs)
    1.67  val dummy_thf_config =
    1.68    dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
    1.69  val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
    1.70 @@ -743,7 +739,7 @@
    1.71    (remote_prefix ^ name,
    1.72     remotify_config system_name system_versions best_slice o config)
    1.73  
    1.74 -val explicit_tff0 = TFF (Monomorphic, TPTP_Explicit)
    1.75 +val explicit_tff0 = TFF Monomorphic
    1.76  
    1.77  val remote_agsyhol =
    1.78    remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
    1.79 @@ -764,7 +760,7 @@
    1.80    remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
    1.81        (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
    1.82  val remote_vampire =
    1.83 -  remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
    1.84 +  remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5", "1.8"]
    1.85        (K (((250, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
    1.86  val remote_e_sine =
    1.87    remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture