--- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200
@@ -993,8 +993,8 @@
atomic_types = atomic_types}
end
-fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc presimp_consts
- ((name, loc), t) =
+fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc
+ presimp_consts ((name, loc), t) =
let val thy = Proof_Context.theory_of ctxt in
case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom
|> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:11:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Jul 17 14:11:35 2011 +0200
@@ -525,6 +525,11 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
+fun lift_lambdas ctxt ts =
+ case SMT_Translate.lift_lambdas ctxt false ts |> snd of
+ (defs, [t]) => [foldr1 HOLogic.mk_conj (t :: defs)] (* FIXME: hack *)
+ | (defs, ts) => ts @ defs
+
fun translate_atp_lambdas ctxt type_enc =
Config.get ctxt atp_lambda_translation
|> (fn trans =>
@@ -537,16 +542,11 @@
else
trans)
|> (fn trans =>
- if trans = concealed_lambdasN then
- map (conceal_lambdas ctxt)
- else if trans = lambda_liftingN then
- I (* TODO: implement *)
- else if trans = combinatorsN then
- map (introduce_combinators ctxt)
- else if trans = lambdasN then
- map Envir.eta_contract
- else
- error ("Unknown lambda translation method: " ^ quote trans ^ "."))
+ if trans = concealed_lambdasN then map (conceal_lambdas ctxt)
+ else if trans = lambda_liftingN then lift_lambdas ctxt
+ else if trans = combinatorsN then map (introduce_combinators ctxt)
+ else if trans = lambdasN then map Envir.eta_contract
+ else error ("Unknown lambda translation method: " ^ quote trans ^ "."))
val metis_minimize_max_time = seconds 2.0