src/HOL/TPTP/atp_export.ML

   let
     val thy = Proof_Context.theory_of ctxt
     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 []) ^ " " ^
       File.shell_path prob_file
   in

               (ordered_names ~~ (1 upto length ordered_names))
     val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
     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
 
 end;