--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 07 07:04:53 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 07 07:06:24 2011 +0200
@@ -70,7 +70,7 @@
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
val is_format_typed : format -> bool
- val tptp_strings_for_atp_problem : format -> string problem -> string list
+ val tptp_lines_for_atp_problem : format -> string problem -> string list
val ensure_cnf_problem :
(string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
@@ -283,7 +283,7 @@
| (_, SOME tm) =>
", " ^ string_for_term format (source |> the_default default_source) ^
", " ^ string_for_term format tm) ^ ").\n"
-fun tptp_strings_for_atp_problem format problem =
+fun tptp_lines_for_atp_problem format problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
maps (fn (_, []) => []