1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     1.3 @@ -1430,35 +1430,34 @@
     1.4                         hyp_ts concl_t facts =
     1.5    let
     1.6      val thy = Proof_Context.theory_of ctxt
     1.7 -    val fact_ts = facts |> map snd
     1.8      val presimp_consts = Meson.presimplified_consts ctxt
     1.9      val preprocess = preprocess_prop ctxt trans_lambdas presimp_consts
    1.10 -    val (facts, fact_names) =
    1.11 -      facts |> map (fn (name, t) =>
    1.12 -                       (name, t |> preproc ? preprocess Axiom)
    1.13 -                       |> make_fact ctxt format type_enc true
    1.14 -                       |> rpair name)
    1.15 -            |> map_filter (try (apfst the))
    1.16 -            |> ListPair.unzip
    1.17 +    val fact_ts = facts |> map snd
    1.18      (* Remove existing facts from the conjecture, as this can dramatically
    1.19         boost an ATP's performance (for some reason). *)
    1.20      val hyp_ts =
    1.21        hyp_ts
    1.22        |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
    1.23 -    val goal_t = Logic.list_implies (hyp_ts, concl_t)
    1.24 -    val all_ts = goal_t :: fact_ts
    1.25 +    val fact_ts = facts |> map snd |> preproc ? map (preprocess Axiom)
    1.26 +    val conj_ps =
    1.27 +      map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
    1.28 +      |> preproc
    1.29 +         ? map (fn (kind, t) => (kind, t |> preprocess kind |> freeze_term))
    1.30 +    val (facts, fact_names) =
    1.31 +      map2 (fn (name, _) => fn t =>
    1.32 +               (make_fact ctxt format type_enc true (name, t), name))
    1.33 +           facts fact_ts
    1.34 +      |> map_filter (try (apfst the))
    1.35 +      |> ListPair.unzip
    1.36 +    val conjs = make_conjecture ctxt format type_enc conj_ps
    1.37 +    val all_ts = concl_t :: hyp_ts @ fact_ts
    1.38      val subs = tfree_classes_of_terms all_ts
    1.39      val supers = tvar_classes_of_terms all_ts
    1.40      val tycons = type_constrs_of_terms thy all_ts
    1.41 -    val conjs =
    1.42 -      map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
    1.43 -      |> preproc
    1.44 -         ? map (fn (kind, t) => (kind, t |> preprocess kind |> freeze_term))
    1.45 -      |> make_conjecture ctxt format type_enc
    1.46 -    val (supers', arity_clauses) =
    1.47 +    val (supers, arity_clauses) =
    1.48        if level_of_type_enc type_enc = No_Types then ([], [])
    1.49        else make_arity_clauses thy tycons supers
    1.50 -    val class_rel_clauses = make_class_rel_clauses thy subs supers'
    1.51 +    val class_rel_clauses = make_class_rel_clauses thy subs supers
    1.52    in
    1.53      (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
    1.54    end