# HG changeset patch
# User boehmes
# Date 1308748023 -7200
# Node ID d566714a9ce1089cd5395506afcf58266d66028e
# Parent  4ffb4ca04fb88b1e3cd5084baa9f276c6daa4c77
export lambda-lifting code as there is potential use for it within Sledgehammer

diff -r 4ffb4ca04fb8 -r d566714a9ce1 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 21 23:08:16 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Jun 22 15:07:03 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) =