--- 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 (_, []) => []
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Jun 07 07:04:53 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Jun 07 07:06:24 2011 +0200
@@ -180,7 +180,7 @@
prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
false false props @{prop False} []
(*
-val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem))
+val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
*)
(* "rev" is for compatibility *)
val axioms =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 07:04:53 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 07 07:06:24 2011 +0200
@@ -652,7 +652,7 @@
"exec " ^ core) ^ " 2>&1"
val _ =
atp_problem
- |> tptp_strings_for_atp_problem format
+ |> tptp_lines_for_atp_problem format
|> cons ("% " ^ command ^ "\n")
|> File.write_list prob_file
val conjecture_shape =
--- a/src/HOL/ex/atp_export.ML Tue Jun 07 07:04:53 2011 +0200
+++ b/src/HOL/ex/atp_export.ML Tue Jun 07 07:06:24 2011 +0200
@@ -114,8 +114,7 @@
val infers =
infers |> map (apsnd (filter (member (op = o apsnd fst) infers)))
val atp_problem = atp_problem |> add_inferences_to_problem infers
- val ss =
- ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.FOF atp_problem
+ val ss = ATP_Problem.tptp_lines_for_atp_problem ATP_Problem.FOF atp_problem
val _ = app (File.append path) ss
in () end