src/HOL/Tools/ATP/atp_problem.ML

   | tptp_string_of_line format (Sym_Decl (ident, sym, ty)) =
     tptp_string_of_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^
     " : " ^ string_of_type format ty ^ ").\n"
   | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, _)) =
     tptp_string_of_format format ^ "(" ^ ident ^ ", " ^
-    tptp_string_of_role kind ^ "," ^ maybe_alt alt ^
-    "\n    (" ^ tptp_string_of_formula format phi ^ ")" ^
+    tptp_string_of_role kind ^ "," ^ "\n    (" ^
+    tptp_string_of_formula format phi ^ ")" ^
     (case source of
-       SOME tm => ", " ^ tptp_string_of_term format tm
-     | NONE => "") ^ ").\n"
+      SOME tm => ", " ^ tptp_string_of_term format tm
+    | NONE => "") ^
+    ")." ^ maybe_alt alt ^ "\n"
 
 fun tptp_lines format =
   maps (fn (_, []) => []
          | (heading, lines) =>
            "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::

       ")."
     fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
     fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
         if pred kind then
           let val rank = extract_isabelle_rank info in
-            "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^
-            ", " ^ ident ^
+            "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^ ", " ^ ident ^
             (if rank = default_rank then "" else ", " ^ string_of_int rank) ^
             ")." ^ maybe_alt alt
             |> SOME
           end
         else