# HG changeset patch
# User blanchet
# Date 1376382416 -7200
# Node ID ab98feb666841a44057261713ac0171953335463
# Parent  fcd3a59c6f7289447178f7e763d2062cdd49fe9e
Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)

diff -r fcd3a59c6f72 -r ab98feb66684 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Tue Aug 13 10:26:56 2013 +0200
@@ -33,12 +33,12 @@
 
 val fact_name_of = prefix fact_prefix o ascii_of
 
-fun atp_of_format (THF (Polymorphic, _, _, _)) = dummy_thfN
-  | atp_of_format (THF (Monomorphic, _, _, _)) = satallaxN
+fun atp_of_format (THF (Polymorphic, _, _)) = dummy_thfN
+  | atp_of_format (THF (Monomorphic, _, _)) = satallaxN
   | atp_of_format (DFG Polymorphic) = spass_polyN
   | atp_of_format (DFG Monomorphic) = spassN
-  | atp_of_format (TFF (Polymorphic, _)) = alt_ergoN
-  | atp_of_format (TFF (Monomorphic, _)) = vampireN
+  | atp_of_format (TFF Polymorphic) = alt_ergoN
+  | atp_of_format (TFF Monomorphic) = vampireN
   | atp_of_format FOF = eN
   | atp_of_format CNF_UEQ = waldmeisterN
   | atp_of_format CNF = eN
diff -r fcd3a59c6f72 -r ab98feb66684 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 13 10:26:56 2013 +0200
@@ -30,7 +30,6 @@
      gen_simp : bool}
 
   datatype polymorphism = Monomorphic | Polymorphic
-  datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
   datatype thf_choice = THF_Without_Choice | THF_With_Choice
   datatype thf_defs = THF_Without_Defs | THF_With_Defs
 
@@ -38,8 +37,8 @@
     CNF |
     CNF_UEQ |
     FOF |
-    TFF of polymorphism * tptp_explicitness |
-    THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
+    TFF of polymorphism |
+    THF of polymorphism * thf_choice * thf_defs |
     DFG of polymorphism
 
   datatype formula_role =
@@ -175,7 +174,6 @@
    gen_simp : bool}
 
 datatype polymorphism = Monomorphic | Polymorphic
-datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
 datatype thf_choice = THF_Without_Choice | THF_With_Choice
 datatype thf_defs = THF_Without_Defs | THF_With_Defs
 
@@ -183,8 +181,8 @@
   CNF |
   CNF_UEQ |
   FOF |
-  TFF of polymorphism * tptp_explicitness |
-  THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
+  TFF of polymorphism |
+  THF of polymorphism * thf_choice * thf_defs |
   DFG of polymorphism
 
 datatype formula_role =
@@ -911,7 +909,7 @@
       if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
     val avoid_clash =
       case format of
-        TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
+        TFF Polymorphic => avoid_clash_with_alt_ergo_type_vars
       | DFG _ => avoid_clash_with_dfg_keywords
       | _ => I
     val nice_name = nice_name avoid_clash
diff -r fcd3a59c6f72 -r ab98feb66684 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Aug 13 10:26:56 2013 +0200
@@ -688,13 +688,13 @@
     Raw_Polymorphic With_Phantom_Type_Vars
   | no_type_classes poly = poly
 
-fun adjust_type_enc (THF (Polymorphic, _, choice, _))
+fun adjust_type_enc (THF (Polymorphic, choice, _))
                     (Native (order, poly, level)) =
     Native (adjust_order choice order, no_type_classes poly, level)
-  | adjust_type_enc (THF (Monomorphic, _, choice, _))
+  | adjust_type_enc (THF (Monomorphic, choice, _))
                          (Native (order, _, level)) =
     Native (adjust_order choice order, Mangled_Monomorphic, level)
-  | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) =
+  | adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) =
     Native (First_Order, Mangled_Monomorphic, level)
   | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
     Native (First_Order, poly, level)
@@ -1308,7 +1308,7 @@
      atomic_types = atomic_Ts}
   end
 
-fun is_format_with_defs (THF (_, _, _, THF_With_Defs)) = true
+fun is_format_with_defs (THF (_, _, THF_With_Defs)) = true
   | is_format_with_defs _ = false
 
 fun make_fact ctxt format type_enc iff_for_eq
@@ -2652,7 +2652,7 @@
             o uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0
                                            sym_tab) sym_tab
 
-val implicit_declsN = "Should-be-implicit typings"
+val implicit_declsN = "Could-be-implicit typings"
 val explicit_declsN = "Explicit typings"
 val uncurried_alias_eqsN = "Uncurried aliases"
 val factsN = "Relevant facts"
@@ -2842,8 +2842,6 @@
                     CNF => ensure_cnf_problem
                   | CNF_UEQ => filter_cnf_ueq_problem
                   | FOF => I
-                  | TFF (_, TPTP_Implicit) => I
-                  | THF (_, TPTP_Implicit, _, _) => I
                   | _ => declare_undeclared_in_problem implicit_declsN)
     val (problem, pool) = problem |> nice_atp_problem readable_names format
     fun add_sym_ary (s, {min_ary, ...} : sym_info) =
diff -r fcd3a59c6f72 -r ab98feb66684 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 13 10:26:56 2013 +0200
@@ -211,8 +211,7 @@
 
 (* agsyHOL *)
 
-val agsyhol_thf0 =
-  THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
+val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
 
 val agsyhol_config : atp_config =
   {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
@@ -233,7 +232,7 @@
 
 (* Alt-Ergo *)
 
-val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
+val alt_ergo_tff1 = TFF Polymorphic
 
 val alt_ergo_config : atp_config =
   {exec = K (["WHY3_HOME"], ["why3"]),
@@ -462,8 +461,7 @@
 
 (* LEO-II supports definitions, but it performs significantly better on our
    benchmarks when they are not used. *)
-val leo2_thf0 =
-  THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
+val leo2_thf0 = THF (Monomorphic, THF_Without_Choice, THF_Without_Defs)
 
 val leo2_config : atp_config =
   {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
@@ -490,8 +488,7 @@
 (* Satallax *)
 
 (* Choice is disabled until there is proper reconstruction for it. *)
-val satallax_thf0 =
-  THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
+val satallax_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
 
 val satallax_config : atp_config =
   {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
@@ -568,7 +565,7 @@
 fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
 fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
 
-val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
+val vampire_tff0 = TFF Monomorphic
 
 val vampire_config : atp_config =
   {exec = K (["VAMPIRE_HOME"], ["vampire"]),
@@ -620,7 +617,7 @@
 
 (* Z3 with TPTP syntax (half experimental, half legacy) *)
 
-val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
+val z3_tff0 = TFF Monomorphic
 
 val z3_tptp_config : atp_config =
   {exec = K (["Z3_HOME"], ["z3"]),
@@ -657,8 +654,7 @@
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
-val dummy_thf_format =
-  THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
+val dummy_thf_format = THF (Polymorphic, THF_With_Choice, THF_With_Defs)
 val dummy_thf_config =
   dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
@@ -743,7 +739,7 @@
   (remote_prefix ^ name,
    remotify_config system_name system_versions best_slice o config)
 
-val explicit_tff0 = TFF (Monomorphic, TPTP_Explicit)
+val explicit_tff0 = TFF Monomorphic
 
 val remote_agsyhol =
   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
@@ -764,7 +760,7 @@
   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
       (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
 val remote_vampire =
-  remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
+  remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5", "1.8"]
       (K (((250, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
diff -r fcd3a59c6f72 -r ab98feb66684 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Tue Aug 13 10:26:56 2013 +0200
@@ -13,7 +13,6 @@
     bool -> preplay_interface -> isar_proof -> isar_proof
 end
 
-
 structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
 struct
 
@@ -107,5 +106,4 @@
     snd (do_proof proof)
   end
 
-
 end