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 @@ -92,8 +92,8 @@
     1.4    val introduce_combinators : Proof.context -> term -> term
     1.5    val prepare_atp_problem :
     1.6      Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
     1.7 -    -> bool -> (term list -> term list) -> bool -> bool -> term list -> term
     1.8 -    -> ((string * locality) * term) list
     1.9 +    -> bool -> ((formula_kind * term) list -> term list) -> bool -> bool
    1.10 +    -> term list -> term -> ((string * locality) * term) list
    1.11      -> string problem * string Symtab.table * int * int
    1.12         * (string * locality) list vector * int list * int Symtab.table
    1.13    val atp_problem_weights : string problem -> (string * real) list
    1.14 @@ -900,7 +900,7 @@
    1.15    else
    1.16      t
    1.17  
    1.18 -fun generic_translate_lambdas do_lambdas ctxt t =
    1.19 +fun simple_translate_lambdas do_lambdas ctxt t =
    1.20    let
    1.21      fun aux Ts t =
    1.22        case t of
    1.23 @@ -932,29 +932,25 @@
    1.24      Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
    1.25            T --> fastype_of1 (Ts, t))
    1.26    | do_conceal_lambdas _ t = t
    1.27 -val conceal_lambdas = generic_translate_lambdas (K do_conceal_lambdas)
    1.28 +val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas)
    1.29  
    1.30 -fun do_introduce_combinators ctxt Ts =
    1.31 +fun do_introduce_combinators ctxt Ts t =
    1.32    let val thy = Proof_Context.theory_of ctxt in
    1.33 -    conceal_bounds Ts
    1.34 -    #> cterm_of thy
    1.35 -    #> Meson_Clausify.introduce_combinators_in_cterm
    1.36 -    #> prop_of #> Logic.dest_equals #> snd
    1.37 -    #> reveal_bounds Ts
    1.38 +    t |> conceal_bounds Ts
    1.39 +      |> cterm_of thy
    1.40 +      |> Meson_Clausify.introduce_combinators_in_cterm
    1.41 +      |> prop_of |> Logic.dest_equals |> snd
    1.42 +      |> reveal_bounds Ts
    1.43    end
    1.44 -val introduce_combinators = generic_translate_lambdas do_introduce_combinators
    1.45 +  (* A type variable of sort "{}" will make abstraction fail. *)
    1.46 +  handle THM _ => do_conceal_lambdas Ts t
    1.47 +val introduce_combinators = simple_translate_lambdas do_introduce_combinators
    1.48  
    1.49 -fun process_abstractions_in_term ctxt trans_lambdas kind t =
    1.50 -  let val thy = Proof_Context.theory_of ctxt in
    1.51 -    if Meson.is_fol_term thy t then
    1.52 -      t
    1.53 -    else
    1.54 -      t |> singleton trans_lambdas
    1.55 -      handle THM _ =>
    1.56 -             (* A type variable of sort "{}" will make abstraction fail. *)
    1.57 -             if kind = Conjecture then HOLogic.false_const
    1.58 -             else HOLogic.true_const
    1.59 -  end
    1.60 +fun process_abstractions_in_terms ctxt trans_lambdas ps =
    1.61 +  let
    1.62 +    val thy = Proof_Context.theory_of ctxt
    1.63 +    val (fo_ps, ho_ps) = ps |> List.partition (Meson.is_fol_term thy o snd)
    1.64 +  in map snd fo_ps @ trans_lambdas ho_ps end
    1.65  
    1.66  (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
    1.67     same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
    1.68 @@ -967,7 +963,7 @@
    1.69        | aux t = t
    1.70    in t |> exists_subterm is_Var t ? aux end
    1.71  
    1.72 -fun preprocess_prop ctxt trans_lambdas presimp_consts kind t =
    1.73 +fun preprocess_prop ctxt presimp_consts t =
    1.74    let
    1.75      val thy = Proof_Context.theory_of ctxt
    1.76      val t = t |> Envir.beta_eta_contract
    1.77 @@ -980,7 +976,6 @@
    1.78        |> extensionalize_term ctxt
    1.79        |> presimplify_term ctxt presimp_consts
    1.80        |> perhaps (try (HOLogic.dest_Trueprop))
    1.81 -      |> process_abstractions_in_term ctxt trans_lambdas kind
    1.82    end
    1.83  
    1.84  (* making fact and conjecture formulas *)
    1.85 @@ -1431,7 +1426,11 @@
    1.86    let
    1.87      val thy = Proof_Context.theory_of ctxt
    1.88      val presimp_consts = Meson.presimplified_consts ctxt
    1.89 -    val preprocess = preprocess_prop ctxt trans_lambdas presimp_consts
    1.90 +    fun preprocess kind =
    1.91 +      preprocess_prop ctxt presimp_consts
    1.92 +      #> pair kind #> single
    1.93 +      #> process_abstractions_in_terms ctxt trans_lambdas
    1.94 +      #> the_single
    1.95      val fact_ts = facts |> map snd
    1.96      (* Remove existing facts from the conjecture, as this can dramatically
    1.97         boost an ATP's performance (for some reason). *)