1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
     1.3 @@ -131,8 +131,7 @@
     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 option -> bool -> bool -> term list -> term
     1.8 -    -> ((string * locality) * term) list
     1.9 +    -> bool -> bool -> term list -> term -> ((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 @@ -1833,9 +1832,10 @@
    1.14  val conjsN = "Conjectures"
    1.15  val free_typesN = "Type variables"
    1.16  
    1.17 +val explicit_apply = NONE (* for experimental purposes *)
    1.18 +
    1.19  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
    1.20 -                        explicit_apply readable_names preproc hyp_ts concl_t
    1.21 -                        facts =
    1.22 +                        readable_names preproc hyp_ts concl_t facts =
    1.23    let
    1.24      val (format, type_sys) = choose_format [format] type_sys
    1.25      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =