make TFF output less explicit where possible

--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 19:09:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 25 22:05:18 2011 +0200
@@ -19,12 +19,13 @@
 
   datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
 
+  datatype tff_flavor = Implicit | Explicit
   datatype thf_flavor = Without_Choice | With_Choice
   datatype format =
     CNF |
     CNF_UEQ |
     FOF |
-    TFF |
+    TFF of tff_flavor |
     THF of thf_flavor
 
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -118,12 +119,14 @@
 
 datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type
 
+datatype tff_flavor = Implicit | Explicit
 datatype thf_flavor = Without_Choice | With_Choice
+
 datatype format =
   CNF |
   CNF_UEQ |
   FOF |
-  TFF |
+  TFF of tff_flavor |
   THF of thf_flavor
 
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
@@ -210,7 +213,7 @@
 
 fun is_format_thf (THF _) = true
   | is_format_thf _ = false
-fun is_format_typed TFF = true
+fun is_format_typed (TFF _) = true
   | is_format_typed (THF _) = true
   | is_format_typed _ = false
 
@@ -232,7 +235,7 @@
           aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2
           |> not rhs ? enclose "(" ")"
     in aux true ty end
-  | string_for_type TFF ty =
+  | string_for_type (TFF _) ty =
     (case strip_tff_type ty of
        ([], s) => s
      | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
@@ -320,7 +323,7 @@
 fun string_for_format CNF = tptp_cnf
   | string_for_format CNF_UEQ = tptp_cnf
   | string_for_format FOF = tptp_fof
-  | string_for_format TFF = tptp_tff
+  | string_for_format (TFF _) = tptp_tff
   | string_for_format (THF _) = tptp_thf
 
 fun string_for_problem_line format (Decl (ident, sym, ty)) =

--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 19:09:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 25 22:05:18 2011 +0200
@@ -338,9 +338,9 @@
          (0.334, (true, (50, FOF, "mono_guards?", no_sosN))),
          (0.333, (false, (500, FOF, "mono_tags?", sosN)))]
       else
-        [(0.333, (false, (150, TFF, "poly_guards", sosN))),
-         (0.334, (true, (50, TFF, "simple", no_sosN))),
-         (0.333, (false, (500, TFF, "simple", sosN)))])
+        [(0.333, (false, (150, TFF Implicit, "poly_guards", sosN))),
+         (0.334, (true, (50, TFF Implicit, "simple", no_sosN))),
+         (0.333, (false, (500, TFF Implicit, "simple", sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -368,8 +368,8 @@
      (* FUDGE *)
      K [(0.5, (false, (250, FOF, "mono_guards?", ""))),
         (0.25, (false, (125, FOF, "mono_guards?", ""))),
-        (0.125, (false, (62, TFF, "simple", ""))),
-        (0.125, (false, (31, TFF, "simple", "")))]}
+        (0.125, (false, (62, TFF Implicit, "simple", ""))),
+        (0.125, (false, (31, TFF Implicit, "simple", "")))]}
 
 val z3_tptp = (z3_tptpN, z3_tptp_config)
 
@@ -457,19 +457,21 @@
   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
                (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
 val remote_vampire =
-  remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
+  remotify_atp vampire "Vampire" ["1.8"]
+               (K (250, TFF Implicit, "simple") (* FUDGE *))
 val remote_z3_tptp =
-  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
+  remotify_atp z3_tptp "Z3" ["3.0"]
+                       (K (250, TFF Implicit, "simple") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
              Conjecture (K (500, FOF, "mono_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
-             (K (100, TFF, "simple") (* FUDGE *))
+             (K (100, TFF Explicit, "simple") (* FUDGE *))
 val remote_e_tofof =
   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *))
+             Axiom Hypothesis (K (150, TFF Explicit, "simple") (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
              [("#START OF PROOF", "Proved Goals:")]

--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 19:09:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 22:05:18 2011 +0200
@@ -621,7 +621,7 @@
   | is_type_level_monotonicity_based _ = false
 
 fun adjust_type_enc (THF _) type_enc = type_enc
-  | adjust_type_enc TFF (Simple_Types (_, level)) =
+  | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
     Simple_Types (First_Order, level)
   | adjust_type_enc format (Simple_Types (_, level)) =
     adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))