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

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:11:34 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:11:35 2011 +0200
     2.3 @@ -525,6 +525,11 @@
     2.4     | NONE => type_enc_from_string best_type_enc)
     2.5    |> choose_format formats
     2.6  
     2.7 +fun lift_lambdas ctxt ts =
     2.8 +  case SMT_Translate.lift_lambdas ctxt false ts |> snd of
     2.9 +    (defs, [t]) => [foldr1 HOLogic.mk_conj (t :: defs)] (* FIXME: hack *)
    2.10 +  | (defs, ts) => ts @ defs
    2.11 +
    2.12  fun translate_atp_lambdas ctxt type_enc =
    2.13    Config.get ctxt atp_lambda_translation
    2.14    |> (fn trans =>
    2.15 @@ -537,16 +542,11 @@
    2.16           else
    2.17             trans)
    2.18    |> (fn trans =>
    2.19 -         if trans = concealed_lambdasN then
    2.20 -           map (conceal_lambdas ctxt)
    2.21 -         else if trans = lambda_liftingN then
    2.22 -           I (* TODO: implement *)
    2.23 -         else if trans = combinatorsN then
    2.24 -           map (introduce_combinators ctxt)
    2.25 -         else if trans = lambdasN then
    2.26 -           map Envir.eta_contract
    2.27 -         else
    2.28 -           error ("Unknown lambda translation method: " ^ quote trans ^ "."))
    2.29 +         if trans = concealed_lambdasN then map (conceal_lambdas ctxt)
    2.30 +         else if trans = lambda_liftingN then lift_lambdas ctxt
    2.31 +         else if trans = combinatorsN then map (introduce_combinators ctxt)
    2.32 +         else if trans = lambdasN then map Envir.eta_contract
    2.33 +         else error ("Unknown lambda translation method: " ^ quote trans ^ "."))
    2.34  
    2.35  val metis_minimize_max_time = seconds 2.0
    2.36