correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i

--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Dec 13 14:55:42 2011 +0100
@@ -107,8 +107,7 @@
     (string * string) problem -> (string * string) problem
   val filter_cnf_ueq_problem :
     (string * string) problem -> (string * string) problem
-  val declare_undeclared_syms_in_atp_problem :
-    string -> string -> (string * string) problem -> (string * string) problem
+  val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list
   val nice_atp_problem :
     bool -> ('a * (string * string) problem_line list) list
     -> ('a * string problem_line list) list
@@ -613,59 +612,11 @@
 
 (** Symbol declarations **)
 
-(* TFF allows implicit declarations of types, function symbols, and predicate
-   symbols (with "$i" as the type of individuals), but some provers (e.g.,
-   SNARK) require explicit declarations. The situation is similar for THF. *)
-fun default_type pred_sym =
-  let
-    fun typ 0 = if pred_sym then bool_atype else individual_atype
-      | typ ary = AFun (individual_atype, typ (ary - 1))
-  in typ end
-
 fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym
   | add_declared_syms_in_problem_line _ = I
 fun declared_syms_in_problem problem =
   fold (fold add_declared_syms_in_problem_line o snd) problem []
 
-fun nary_type_constr_type n =
-  funpow n (curry AFun atype_of_types) atype_of_types
-
-fun undeclared_syms_in_problem declared problem =
-  let
-    fun do_sym name ty =
-      if member (op =) declared name then I else AList.default (op =) (name, ty)
-    fun do_type (AType (name as (s, _), tys)) =
-        is_tptp_user_symbol s
-        ? do_sym name (fn _ => nary_type_constr_type (length tys))
-        #> fold do_type tys
-      | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
-      | do_type (ATyAbs (_, ty)) = do_type ty
-    fun do_term pred_sym (ATerm (name as (s, _), tms)) =
-        is_tptp_user_symbol s
-        ? do_sym name (fn _ => default_type pred_sym (length tms))
-        #> fold (do_term false) tms
-      | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
-    fun do_formula (AQuant (_, xs, phi)) =
-        fold do_type (map_filter snd xs) #> do_formula phi
-      | do_formula (AConn (_, phis)) = fold do_formula phis
-      | do_formula (AAtom tm) = do_term true tm
-    fun do_problem_line (Decl (_, _, ty)) = do_type ty
-      | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
-  in
-    fold (fold do_problem_line o snd) problem []
-    |> filter_out (is_built_in_tptp_symbol o fst o fst)
-  end
-
-fun declare_undeclared_syms_in_atp_problem prefix heading problem =
-  let
-    fun decl_line (x as (s, _), ty) = Decl (prefix ^ s, x, ty ())
-    val declared = problem |> declared_syms_in_problem
-    val decls =
-      problem |> undeclared_syms_in_problem declared
-              |> sort_wrt (fst o fst)
-              |> map decl_line
-  in (heading, decls) :: problem end
-
 (** Nice names **)
 
 fun empty_name_pool readable_names =

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:55:42 2011 +0100
@@ -2333,6 +2333,58 @@
 val conjsN = "Conjectures"
 val free_typesN = "Type variables"
 
+(* TFF allows implicit declarations of types, function symbols, and predicate
+   symbols (with "$i" as the type of individuals), but some provers (e.g.,
+   SNARK) require explicit declarations. The situation is similar for THF. *)
+
+fun default_type pred_sym s =
+  let
+    val ind =
+      if String.isPrefix type_const_prefix s then atype_of_types
+      else individual_atype
+    fun typ 0 = if pred_sym then bool_atype else ind
+      | typ ary = AFun (ind, typ (ary - 1))
+  in typ end
+
+fun nary_type_constr_type n =
+  funpow n (curry AFun atype_of_types) atype_of_types
+
+fun undeclared_syms_in_problem problem =
+  let
+    val declared = declared_syms_in_problem problem
+    fun do_sym name ty =
+      if member (op =) declared name then I else AList.default (op =) (name, ty)
+    fun do_type (AType (name as (s, _), tys)) =
+        is_tptp_user_symbol s
+        ? do_sym name (fn () => nary_type_constr_type (length tys))
+        #> fold do_type tys
+      | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
+      | do_type (ATyAbs (_, ty)) = do_type ty
+    fun do_term pred_sym (ATerm (name as (s, _), tms)) =
+        is_tptp_user_symbol s
+        ? do_sym name (fn _ => default_type pred_sym s (length tms))
+        #> fold (do_term false) tms
+      | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
+    fun do_formula (AQuant (_, xs, phi)) =
+        fold do_type (map_filter snd xs) #> do_formula phi
+      | do_formula (AConn (_, phis)) = fold do_formula phis
+      | do_formula (AAtom tm) = do_term true tm
+    fun do_problem_line (Decl (_, _, ty)) = do_type ty
+      | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
+  in
+    fold (fold do_problem_line o snd) problem []
+    |> filter_out (is_built_in_tptp_symbol o fst o fst)
+  end
+
+fun declare_undeclared_syms_in_atp_problem problem =
+  let
+    val decls =
+      problem
+      |> undeclared_syms_in_problem
+      |> sort_wrt (fst o fst)
+      |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
+  in (implicit_declsN, decls) :: problem end
+
 val explicit_apply_threshold = 50
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
@@ -2411,8 +2463,7 @@
           | FOF => I
           | TFF (_, TPTP_Implicit) => I
           | THF (_, TPTP_Implicit, _) => I
-          | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
-                                                        implicit_declsN)
+          | _ => declare_undeclared_syms_in_atp_problem)
     val (problem, pool) = problem |> nice_atp_problem readable_names
     fun add_sym_ary (s, {min_ary, ...} : sym_info) =
       min_ary > 0 ? Symtab.insert (op =) (s, min_ary)