# HG changeset patch
# User blanchet
# Date 1307423184 -7200
# Node ID 97906dfd39b76caf6f8f8b91d459d7539ddf3da1
# Parent  c9e87dc92d9ec7f7e000bc46a2ae023f635b6e6a
renamed ML function

diff -r c9e87dc92d9e -r 97906dfd39b7 src/HOL/Tools/ATP/atp_problem.ML
--- 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 (_, []) => []
diff -r c9e87dc92d9e -r 97906dfd39b7 src/HOL/Tools/Metis/metis_translate.ML
--- 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 =
diff -r c9e87dc92d9e -r 97906dfd39b7 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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 =
diff -r c9e87dc92d9e -r 97906dfd39b7 src/HOL/ex/atp_export.ML
--- 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