--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 24 12:36:45 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 24 12:36:45 2014 +0200
@@ -437,7 +437,9 @@
let
val of_type = string_of_type format
val of_term = tptp_string_of_term format
- fun app () = tptp_string_of_app format s (map of_type tys @ map of_term ts)
+ fun app () =
+ tptp_string_of_app format s
+ (map (of_type #> is_format_higher_order format ? parens) tys @ map of_term ts)
in
if s = tptp_empty_list then
(* used for lists in the optional "source" field of a derivation *)