# HG changeset patch # User wenzelm # Date 1308753331 -7200 # Node ID bbbd6cad7df17394caf5efd35b89d4b71cd9eb88 # Parent d566714a9ce1089cd5395506afcf58266d66028e# Parent bf7400573617fe27f0c2faea91eb28ce4215737c merged diff -r bf7400573617 -r bbbd6cad7df1 src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Wed Jun 22 16:32:36 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Jun 22 16:35:31 2011 +0200 @@ -38,6 +38,8 @@ (*translation*) val add_config: SMT_Utils.class * (Proof.context -> config) -> Context.generic -> Context.generic + val lift_lambdas: Proof.context -> term list -> + Proof.context * (term list * term list) val translate: Proof.context -> string list -> (int * thm) list -> string * recon end @@ -308,7 +310,7 @@ (Termtab.empty, ctxt) |> fold_map (traverse []) ts |> (fn (us, (defs, ctxt')) => - (ctxt', Termtab.fold (cons o snd o snd) defs us)) + (ctxt', (Termtab.fold (cons o snd o snd) defs [], us))) end @@ -588,6 +590,7 @@ ts2 |> eta_expand ctxt1 is_fol funcs |> lift_lambdas ctxt1 + ||> (op @) |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs) val ((rewrite_rules, extra_thms, builtin), ts4) =