1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 00:16:28 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 00:16:28 2011 +0200
     1.3 @@ -130,7 +130,8 @@
     1.4    val type_constrs_of_terms : theory -> term list -> string list
     1.5    val prepare_atp_problem :
     1.6      Proof.context -> format -> formula_kind -> formula_kind -> type_sys
     1.7 -    -> bool -> bool -> term list -> term -> ((string * locality) * term) list
     1.8 +    -> bool -> bool -> bool -> term list -> term
     1.9 +    -> ((string * locality) * term) list
    1.10      -> string problem * string Symtab.table * int * int
    1.11         * (string * locality) list vector * int list * int Symtab.table
    1.12    val atp_problem_weights : string problem -> (string * real) list
    1.13 @@ -1547,12 +1548,8 @@
    1.14     the remote provers might care. *)
    1.15  fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
    1.16                            (j, formula as {name, locality, kind, ...}) =
    1.17 -  Formula (prefix ^
    1.18 -           (if freshen andalso
    1.19 -               polymorphism_of_type_sys type_sys <> Polymorphic then
    1.20 -              string_of_int j ^ "_"
    1.21 -            else
    1.22 -              "") ^ encode name,
    1.23 +  Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
    1.24 +           encode name,
    1.25             kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
    1.26             case locality of
    1.27               Intro => intro_info
    1.28 @@ -1838,7 +1835,7 @@
    1.29  val explicit_apply = NONE (* for experimental purposes *)
    1.30  
    1.31  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
    1.32 -                        readable_names preproc hyp_ts concl_t facts =
    1.33 +        freshen_facts readable_names preproc hyp_ts concl_t facts =
    1.34    let
    1.35      val (format, type_sys) = choose_format [format] type_sys
    1.36      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
    1.37 @@ -1877,8 +1874,8 @@
    1.38      val problem =
    1.39        [(explicit_declsN, sym_decl_lines),
    1.40         (factsN,
    1.41 -        map (formula_line_for_fact ctxt format fact_prefix ascii_of true
    1.42 -                                   nonmono_Ts type_sys)
    1.43 +        map (formula_line_for_fact ctxt format fact_prefix ascii_of
    1.44 +                                   freshen_facts nonmono_Ts type_sys)
    1.45              (0 upto length facts - 1 ~~ facts)),
    1.46         (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
    1.47         (aritiesN, map formula_line_for_arity_clause arity_clauses),