--- 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