diff -r da014b00d7a4 -r fe291ab75eb5 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu May 26 23:21:00 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri May 27 10:30:07 2011 +0200
@@ -160,7 +160,8 @@
        ([], s) => s
      | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
      | (ss, s) =>
-       "(" ^ space_implode tptp_prod_type ss ^ ") " ^ tptp_fun_type ^ " " ^ s)
+       "(" ^ space_implode (" " ^ tptp_prod_type ^ " ") ss ^ ") " ^
+       tptp_fun_type ^ " " ^ s)
   | string_for_type _ _ = raise Fail "unexpected type in untyped format"
 
 fun string_for_term _ (ATerm (s, [])) = s