1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:34 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     1.3 @@ -993,8 +993,8 @@
     1.4       atomic_types = atomic_types}
     1.5    end
     1.6  
     1.7 -fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc presimp_consts
     1.8 -              ((name, loc), t) =
     1.9 +fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc
    1.10 +              presimp_consts ((name, loc), t) =
    1.11    let val thy = Proof_Context.theory_of ctxt in
    1.12      case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom
    1.13             |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name