diff -r 6a9458524f01 -r a15f0db2bcaf src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
@@ -18,6 +18,7 @@
 
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
+    Type_Decl of string * 'a * 'a list * 'a |
     Formula of string * formula_kind * ('a, 'a fo_term) formula
                * string fo_term option
   type 'a problem = (string * 'a problem_line list) list
@@ -48,6 +49,7 @@
 
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
+  Type_Decl of string * 'a * 'a list * 'a |
   Formula of string * formula_kind * ('a, 'a fo_term) formula
              * string fo_term option
 type 'a problem = (string * 'a problem_line list) list
@@ -98,22 +100,30 @@
     exists formula_needs_typed_logic phis
   | formula_needs_typed_logic (AAtom _) = false
 
-fun string_for_problem_line use_conjecture_for_hypotheses
+fun string_for_symbol_type [] res_ty = res_ty
+  | string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
+  | string_for_symbol_type arg_tys res_ty =
+    string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty
+
+fun string_for_problem_line _ (Type_Decl (ident, sym, arg_tys, res_ty)) =
+    "tff(" ^ ident ^ ", type, " ^ sym ^ " : " ^
+    string_for_symbol_type arg_tys res_ty ^ ").\n"
+  | string_for_problem_line use_conjecture_for_hypotheses
                             (Formula (ident, kind, phi, source)) =
-  let
-    val (kind, phi) =
-      if kind = Hypothesis andalso use_conjecture_for_hypotheses then
-        (Conjecture, AConn (ANot, [phi]))
-      else
-        (kind, phi)
-  in
-    (if formula_needs_typed_logic phi then "tff" else "fof") ^
-    "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
-    string_for_formula phi ^ ")" ^
-    (case source of
-       SOME tm => ", " ^ string_for_term tm
-     | NONE => "") ^ ").\n"
-  end
+    let
+      val (kind, phi) =
+        if kind = Hypothesis andalso use_conjecture_for_hypotheses then
+          (Conjecture, AConn (ANot, [phi]))
+        else
+          (kind, phi)
+    in
+      (if formula_needs_typed_logic phi then "tff" else "fof") ^
+      "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
+      string_for_formula phi ^ ")" ^
+      (case source of
+         SOME tm => ", " ^ string_for_term tm
+       | NONE => "") ^ ").\n"
+    end
 fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
   \% " ^ timestamp () ^ "\n" ::
@@ -194,8 +204,13 @@
   | nice_formula (AConn (c, phis)) =
     pool_map nice_formula phis #>> curry AConn c
   | nice_formula (AAtom tm) = nice_term tm #>> AAtom
-fun nice_problem_line (Formula (ident, kind, phi, source)) =
-  nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source))
+fun nice_problem_line (Type_Decl (ident, sym, arg_tys, res_ty)) =
+    nice_name sym
+    ##>> pool_map nice_name arg_tys
+    ##>> nice_name res_ty
+    #>> (fn ((sym, arg_tys), res_ty) => Type_Decl (ident, sym, arg_tys, res_ty))
+  | nice_problem_line (Formula (ident, kind, phi, source)) =
+    nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source))
 fun nice_problem problem =
   pool_map (fn (heading, lines) =>
                pool_map nice_problem_line lines #>> pair heading) problem