diff -r 6a3b5085fb8f -r 8b87114357bd src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 16 19:41:42 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 16 19:42:44 2014 +0200
@@ -155,7 +155,6 @@
 
 open ATP_Util
 
-
 val parens = enclose "(" ")"
 
 (** ATP problem **)
@@ -385,8 +384,7 @@
 
 val dfg_individual_type = "iii" (* cannot clash *)
 
-val suffix_type_of_types =
-  suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
+val suffix_type_of_types = suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
 
 fun str_of_type format ty =
   let
@@ -439,9 +437,7 @@
     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 tys @ map of_term ts)
     in
       if s = tptp_empty_list then
         (* used for lists in the optional "source" field of a derivation *)