# HG changeset patch
# User blanchet
# Date 1314773350 -7200
# Node ID 49e7dbaf19aa3761fba509de55cc2976bc623868
# Parent  fd520fa2fb09f36d7e99d0d920e2c2c6222f1c7a
fixed explicit declaration of TFF1 types

diff -r fd520fa2fb09 -r 49e7dbaf19aa src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 30 20:10:48 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Aug 31 08:49:10 2011 +0200
@@ -479,14 +479,19 @@
 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_name name = do_sym name (K atype_of_types)
-    fun do_type (AType (name, tys)) = do_type_name name #> fold do_type tys
+    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 (names, ty)) = fold do_type_name names #> do_type ty
+      | 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))