# HG changeset patch
# User blanchet
# Date 1308669459 -7200
# Node ID 0e422a84d0b25d1158ad671357fc5d586b83d55a
# Parent  4c357b7aa7101a08d00aae7cc7d918331cb0ae89
don't change the way helpers are generated for the exporter's sake

diff -r 4c357b7aa710 -r 0e422a84d0b2 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 21 17:17:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 21 17:17:39 2011 +0200
@@ -85,6 +85,7 @@
   val unmangled_const : string -> string * string fo_term list
   val unmangled_const_name : string -> string
   val helper_table : ((string * bool) * thm list) list
+  val factsN : string
   val prepare_atp_problem :
     Proof.context -> format -> formula_kind -> formula_kind -> type_sys
     -> bool -> bool -> bool -> term list -> term
@@ -1516,15 +1517,15 @@
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
-fun formula_line_for_fact ctxt format prefix encode exporter nonmono_Ts type_sys
-                          (j, {name, locality, kind, combformula, atomic_types}) =
-  (prefix ^ (if exporter then "" else string_of_int j ^ "_") ^ encode name,
+fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
+        type_sys (j, {name, locality, kind, combformula, atomic_types}) =
+  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
    kind,
    combformula
    |> close_combformula_universally
    |> formula_from_combformula ctxt format nonmono_Ts type_sys
                                should_predicate_on_var_in_formula
-                               (if exporter then NONE else SOME true)
+                               (if pos then SOME true else NONE)
    |> bound_tvars type_sys atomic_types
    |> close_formula_universally,
    NONE,
@@ -1845,7 +1846,7 @@
                                                poly_nonmono_Ts type_sys
     val helper_lines =
       0 upto length helpers - 1 ~~ helpers
-      |> map (formula_line_for_fact ctxt format helper_prefix I exporter
+      |> map (formula_line_for_fact ctxt format helper_prefix I false true
                                     poly_nonmono_Ts type_sys)
       |> (if needs_type_tag_idempotence type_sys then
             cons (type_tag_idempotence_fact ())
@@ -1856,8 +1857,9 @@
     val problem =
       [(explicit_declsN, sym_decl_lines),
        (factsN,
-        map (formula_line_for_fact ctxt format fact_prefix ascii_of exporter
-                                   nonmono_Ts type_sys)
+        map (formula_line_for_fact ctxt format fact_prefix ascii_of
+                                   (not exporter) (not exporter) nonmono_Ts
+                                   type_sys)
             (0 upto length facts - 1 ~~ facts)),
        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
        (aritiesN, map formula_line_for_arity_clause arity_clauses),