diff -r ae82943481e9 -r 444d111bde7d 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:46 2011 +0200
@@ -74,6 +74,9 @@
   val is_built_in_tptp_symbol : string -> bool
   val is_tptp_variable : string -> bool
   val is_tptp_user_symbol : string -> bool
+  val atype_of_types : (string * string) ho_type
+  val bool_atype : (string * string) ho_type
+  val individual_atype : (string * string) ho_type
   val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
   val mk_aconn :
     connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula