1.1 --- a/src/HOL/TPTP/atp_export.ML	Sun Jul 17 14:11:35 2011 +0200
     1.2 +++ b/src/HOL/TPTP/atp_export.ML	Sun Jul 17 14:11:35 2011 +0200
     1.3 @@ -160,8 +160,8 @@
     1.4        facts
     1.5        |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
     1.6        |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
     1.7 -                             (map (introduce_combinators ctxt)) false true []
     1.8 -                             @{prop False}
     1.9 +                             (map (introduce_combinators ctxt o snd)) false true
    1.10 +                             [] @{prop False}
    1.11      val atp_problem =
    1.12        atp_problem
    1.13        |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     2.3 @@ -92,8 +92,8 @@
     2.4    val introduce_combinators : Proof.context -> term -> term
     2.5    val prepare_atp_problem :
     2.6      Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
     2.7 -    -> bool -> (term list -> term list) -> bool -> bool -> term list -> term
     2.8 -    -> ((string * locality) * term) list
     2.9 +    -> bool -> ((formula_kind * term) list -> term list) -> bool -> bool
    2.10 +    -> term list -> term -> ((string * locality) * term) list
    2.11      -> string problem * string Symtab.table * int * int
    2.12         * (string * locality) list vector * int list * int Symtab.table
    2.13    val atp_problem_weights : string problem -> (string * real) list
    2.14 @@ -900,7 +900,7 @@
    2.15    else
    2.16      t
    2.17  
    2.18 -fun generic_translate_lambdas do_lambdas ctxt t =
    2.19 +fun simple_translate_lambdas do_lambdas ctxt t =
    2.20    let
    2.21      fun aux Ts t =
    2.22        case t of
    2.23 @@ -932,29 +932,25 @@
    2.24      Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
    2.25            T --> fastype_of1 (Ts, t))
    2.26    | do_conceal_lambdas _ t = t
    2.27 -val conceal_lambdas = generic_translate_lambdas (K do_conceal_lambdas)
    2.28 +val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas)
    2.29  
    2.30 -fun do_introduce_combinators ctxt Ts =
    2.31 +fun do_introduce_combinators ctxt Ts t =
    2.32    let val thy = Proof_Context.theory_of ctxt in
    2.33 -    conceal_bounds Ts
    2.34 -    #> cterm_of thy
    2.35 -    #> Meson_Clausify.introduce_combinators_in_cterm
    2.36 -    #> prop_of #> Logic.dest_equals #> snd
    2.37 -    #> reveal_bounds Ts
    2.38 +    t |> conceal_bounds Ts
    2.39 +      |> cterm_of thy
    2.40 +      |> Meson_Clausify.introduce_combinators_in_cterm
    2.41 +      |> prop_of |> Logic.dest_equals |> snd
    2.42 +      |> reveal_bounds Ts
    2.43    end
    2.44 -val introduce_combinators = generic_translate_lambdas do_introduce_combinators
    2.45 +  (* A type variable of sort "{}" will make abstraction fail. *)
    2.46 +  handle THM _ => do_conceal_lambdas Ts t
    2.47 +val introduce_combinators = simple_translate_lambdas do_introduce_combinators
    2.48  
    2.49 -fun process_abstractions_in_term ctxt trans_lambdas kind t =
    2.50 -  let val thy = Proof_Context.theory_of ctxt in
    2.51 -    if Meson.is_fol_term thy t then
    2.52 -      t
    2.53 -    else
    2.54 -      t |> singleton trans_lambdas
    2.55 -      handle THM _ =>
    2.56 -             (* A type variable of sort "{}" will make abstraction fail. *)
    2.57 -             if kind = Conjecture then HOLogic.false_const
    2.58 -             else HOLogic.true_const
    2.59 -  end
    2.60 +fun process_abstractions_in_terms ctxt trans_lambdas ps =
    2.61 +  let
    2.62 +    val thy = Proof_Context.theory_of ctxt
    2.63 +    val (fo_ps, ho_ps) = ps |> List.partition (Meson.is_fol_term thy o snd)
    2.64 +  in map snd fo_ps @ trans_lambdas ho_ps end
    2.65  
    2.66  (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
    2.67     same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
    2.68 @@ -967,7 +963,7 @@
    2.69        | aux t = t
    2.70    in t |> exists_subterm is_Var t ? aux end
    2.71  
    2.72 -fun preprocess_prop ctxt trans_lambdas presimp_consts kind t =
    2.73 +fun preprocess_prop ctxt presimp_consts t =
    2.74    let
    2.75      val thy = Proof_Context.theory_of ctxt
    2.76      val t = t |> Envir.beta_eta_contract
    2.77 @@ -980,7 +976,6 @@
    2.78        |> extensionalize_term ctxt
    2.79        |> presimplify_term ctxt presimp_consts
    2.80        |> perhaps (try (HOLogic.dest_Trueprop))
    2.81 -      |> process_abstractions_in_term ctxt trans_lambdas kind
    2.82    end
    2.83  
    2.84  (* making fact and conjecture formulas *)
    2.85 @@ -1431,7 +1426,11 @@
    2.86    let
    2.87      val thy = Proof_Context.theory_of ctxt
    2.88      val presimp_consts = Meson.presimplified_consts ctxt
    2.89 -    val preprocess = preprocess_prop ctxt trans_lambdas presimp_consts
    2.90 +    fun preprocess kind =
    2.91 +      preprocess_prop ctxt presimp_consts
    2.92 +      #> pair kind #> single
    2.93 +      #> process_abstractions_in_terms ctxt trans_lambdas
    2.94 +      #> the_single
    2.95      val fact_ts = facts |> map snd
    2.96      (* Remove existing facts from the conjecture, as this can dramatically
    2.97         boost an ATP's performance (for some reason). *)

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     3.3 @@ -197,8 +197,8 @@
     3.4      *)
     3.5      val (atp_problem, _, _, _, _, _, sym_tab) =
     3.6        prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
     3.7 -                          (map (introduce_combinators ctxt)) false false []
     3.8 -                          @{prop False} props
     3.9 +                          (map (introduce_combinators ctxt o snd)) false false
    3.10 +                          [] @{prop False} props
    3.11      (*
    3.12      val _ = tracing ("ATP PROBLEM: " ^
    3.13                       cat_lines (tptp_lines_for_atp_problem CNF atp_problem))

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:11:35 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:11:35 2011 +0200
     4.3 @@ -525,10 +525,14 @@
     4.4     | NONE => type_enc_from_string best_type_enc)
     4.5    |> choose_format formats
     4.6  
     4.7 -fun lift_lambdas ctxt ts =
     4.8 -  case SMT_Translate.lift_lambdas ctxt false ts |> snd of
     4.9 -    (defs, [t]) => [foldr1 HOLogic.mk_conj (t :: defs)] (* FIXME: hack *)
    4.10 -  | (defs, ts) => ts @ defs
    4.11 +fun lift_lambdas ctxt ps =
    4.12 +  let
    4.13 +    val ts = map snd ps (*###*)
    4.14 +  in
    4.15 +    case SMT_Translate.lift_lambdas ctxt false ts |> snd of
    4.16 +      (defs, [t]) => [foldr1 HOLogic.mk_conj (t :: defs)] (* FIXME: hack *)
    4.17 +    | (defs, ts) => ts @ defs
    4.18 +  end
    4.19  
    4.20  fun translate_atp_lambdas ctxt type_enc =
    4.21    Config.get ctxt atp_lambda_translation
    4.22 @@ -542,11 +546,16 @@
    4.23           else
    4.24             trans)
    4.25    |> (fn trans =>
    4.26 -         if trans = concealed_lambdasN then map (conceal_lambdas ctxt)
    4.27 -         else if trans = lambda_liftingN then lift_lambdas ctxt
    4.28 -         else if trans = combinatorsN then map (introduce_combinators ctxt)
    4.29 -         else if trans = lambdasN then map Envir.eta_contract
    4.30 -         else error ("Unknown lambda translation method: " ^ quote trans ^ "."))
    4.31 +         if trans = concealed_lambdasN then
    4.32 +           map (conceal_lambdas ctxt o snd)
    4.33 +         else if trans = lambda_liftingN then
    4.34 +           lift_lambdas ctxt
    4.35 +         else if trans = combinatorsN then
    4.36 +           map (introduce_combinators ctxt o snd)
    4.37 +         else if trans = lambdasN then
    4.38 +           map (Envir.eta_contract o snd)
    4.39 +         else
    4.40 +           error ("Unknown lambda translation method: " ^ quote trans ^ "."))
    4.41  
    4.42  val metis_minimize_max_time = seconds 2.0
    4.43