1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 21 17:17:39 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 21 17:17:39 2011 +0200
     1.3 @@ -85,6 +85,7 @@
     1.4    val unmangled_const : string -> string * string fo_term list
     1.5    val unmangled_const_name : string -> string
     1.6    val helper_table : ((string * bool) * thm list) list
     1.7 +  val factsN : string
     1.8    val prepare_atp_problem :
     1.9      Proof.context -> format -> formula_kind -> formula_kind -> type_sys
    1.10      -> bool -> bool -> bool -> term list -> term
    1.11 @@ -1516,15 +1517,15 @@
    1.12  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    1.13     of monomorphization). The TPTP explicitly forbids name clashes, and some of
    1.14     the remote provers might care. *)
    1.15 -fun formula_line_for_fact ctxt format prefix encode exporter nonmono_Ts type_sys
    1.16 -                          (j, {name, locality, kind, combformula, atomic_types}) =
    1.17 -  (prefix ^ (if exporter then "" else string_of_int j ^ "_") ^ encode name,
    1.18 +fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
    1.19 +        type_sys (j, {name, locality, kind, combformula, atomic_types}) =
    1.20 +  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
    1.21     kind,
    1.22     combformula
    1.23     |> close_combformula_universally
    1.24     |> formula_from_combformula ctxt format nonmono_Ts type_sys
    1.25                                 should_predicate_on_var_in_formula
    1.26 -                               (if exporter then NONE else SOME true)
    1.27 +                               (if pos then SOME true else NONE)
    1.28     |> bound_tvars type_sys atomic_types
    1.29     |> close_formula_universally,
    1.30     NONE,
    1.31 @@ -1845,7 +1846,7 @@
    1.32                                                 poly_nonmono_Ts type_sys
    1.33      val helper_lines =
    1.34        0 upto length helpers - 1 ~~ helpers
    1.35 -      |> map (formula_line_for_fact ctxt format helper_prefix I exporter
    1.36 +      |> map (formula_line_for_fact ctxt format helper_prefix I false true
    1.37                                      poly_nonmono_Ts type_sys)
    1.38        |> (if needs_type_tag_idempotence type_sys then
    1.39              cons (type_tag_idempotence_fact ())
    1.40 @@ -1856,8 +1857,9 @@
    1.41      val problem =
    1.42        [(explicit_declsN, sym_decl_lines),
    1.43         (factsN,
    1.44 -        map (formula_line_for_fact ctxt format fact_prefix ascii_of exporter
    1.45 -                                   nonmono_Ts type_sys)
    1.46 +        map (formula_line_for_fact ctxt format fact_prefix ascii_of
    1.47 +                                   (not exporter) (not exporter) nonmono_Ts
    1.48 +                                   type_sys)
    1.49              (0 upto length facts - 1 ~~ facts)),
    1.50         (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
    1.51         (aritiesN, map formula_line_for_arity_clause arity_clauses),