--- a/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:15:58 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:15:58 2011 +0200
@@ -115,8 +115,7 @@
val prob_file = File.tmp_path (Path.explode "prob.tptp")
val {exec, arguments, proof_delims, known_failures, ...} =
get_atp thy spassN
- val _ = problem |> tptp_lines_for_atp_problem FOF
- |> File.write_list prob_file
+ val _ = problem |> lines_for_atp_problem FOF |> File.write_list prob_file
val command =
File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
" " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
@@ -189,7 +188,7 @@
val atp_problem =
atp_problem |> add_inferences_to_problem infers
|> order_problem_facts name_ord
- val ss = tptp_lines_for_atp_problem FOF atp_problem
+ val ss = lines_for_atp_problem FOF atp_problem
val _ = app (File.append path) ss
in () end