diff -r ccf40af26ae9 -r ae82943481e9 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:07:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 16:07:45 2011 +0200
@@ -19,7 +19,8 @@
 
   datatype 'a ho_type =
     AType of 'a * 'a ho_type list |
-    AFun of 'a ho_type * 'a ho_type
+    AFun of 'a ho_type * 'a ho_type |
+    ATyAbs of 'a list * 'a ho_type
 
   datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
   datatype tff_explicitness = TFF_Implicit | TFF_Explicit
@@ -122,7 +123,8 @@
 
 datatype 'a ho_type =
   AType of 'a * 'a ho_type list |
-  AFun of 'a ho_type * 'a ho_type
+  AFun of 'a ho_type * 'a ho_type |
+  ATyAbs of 'a list * 'a ho_type
 
 datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic
 datatype tff_explicitness = TFF_Implicit | TFF_Explicit
@@ -229,29 +231,38 @@
   | string_for_kind Hypothesis = "hypothesis"
   | string_for_kind Conjecture = "conjecture"
 
-fun strip_tff_type (AFun (AFun _, _)) =
+fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
+  | flatten_type (ty as AFun (ty1 as AType _, ty2)) =
+    (case flatten_type ty2 of
+       AFun (ty' as AType (s, tys), ty) =>
+       AFun (AType (tptp_product_type,
+                    ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
+     | _ => ty)
+  | flatten_type (ty as AType _) = ty
+  | flatten_type _ =
     raise Fail "unexpected higher-order type in first-order format"
-  | strip_tff_type (AFun (ty1, ty2)) = strip_tff_type ty2 |>> cons ty1
-  | strip_tff_type ty = ([], ty)
 
-fun general_string_for_type ty =
+fun str_for_type ty =
   let
     fun str _ (AType (s, [])) = s
-      | str _ (AType (s, tys)) = s ^ "(" ^ commas (map (str false) tys) ^ ")"
+      | str _ (AType (s, tys)) =
+        tys |> map (str false) 
+            |> (if s = tptp_product_type then
+                  space_implode (" " ^ tptp_product_type ^ " ")
+                  #> length tys > 1 ? enclose "(" ")"
+                else
+                  commas #> enclose "(" ")" #> prefix s)
       | str rhs (AFun (ty1, ty2)) =
         str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
         |> not rhs ? enclose "(" ")"
+      | str _ (ATyAbs (ss, ty)) =
+        tptp_forall ^ "[" ^
+        commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
+                    ss) ^ "] : " ^ str false ty
   in str true ty end
 
-fun string_for_type (THF0 _) ty = general_string_for_type ty
-  | string_for_type (TFF _) ty =
-    (case strip_tff_type ty of
-       ([], ty) => general_string_for_type ty
-     | ([ty1], ty2) => general_string_for_type (AFun (ty1, ty2))
-     | (tys, ty) =>
-       "(" ^ space_implode (" " ^ tptp_product_type ^ " ")
-       (map general_string_for_type tys) ^ ") " ^ tptp_fun_type ^ " " ^
-       general_string_for_type ty)
+fun string_for_type (THF0 _) ty = str_for_type ty
+  | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
   | string_for_type _ _ = raise Fail "unexpected type in untyped format"
 
 fun string_for_quantifier AForall = tptp_forall
@@ -469,9 +480,10 @@
   let
     fun do_sym name ty =
       if member (op =) declared name then I else AList.default (op =) (name, ty)
-    fun do_type (AType (name, tys)) =
-        do_sym name (K atype_of_types) #> fold do_type tys
+    fun do_type_name name = do_sym name (K atype_of_types)
+    fun do_type (AType (name, tys)) = do_type_name name #> fold do_type tys
       | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
+      | do_type (ATyAbs (names, ty)) = fold do_type_name names #> 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))
@@ -571,6 +583,8 @@
 fun nice_type (AType (name, tys)) =
     nice_name name ##>> pool_map nice_type tys #>> AType
   | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
+  | nice_type (ATyAbs (names, ty)) =
+    pool_map nice_name names ##>> nice_type ty #>> ATyAbs
 fun nice_term (ATerm (name, ts)) =
     nice_name name ##>> pool_map nice_term ts #>> ATerm
   | nice_term (AAbs ((name, ty), tm)) =