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