# HG changeset patch
# User blanchet
# Date 1407406661 -7200
# Node ID faab5feffb426c9c2a3a652adc41d39ae6d64f18
# Parent  2479dc4ef90b15ec2da7dcafdfb7c81c64f21d70
put comments between TPTP lines to comply with TPTP BNF

diff -r 2479dc4ef90b -r faab5feffb42 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -537,11 +537,12 @@
     " : " ^ 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 (_, []) => []
@@ -642,8 +643,7 @@
     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