# HG changeset patch
# User boehmes
# Date 1292502868 -3600
# Node ID edab1efe0a7086d1668ab9d107f123b273248e70
# Parent  d23af676f9f8097a2ac483e3c4d4dfe0553dd25f
fix lambda-lifting: take level of bound variables into account and also apply bound variables from outer scope

diff -r d23af676f9f8 -r edab1efe0a70 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:33:06 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 13:34:28 2010 +0100
@@ -254,16 +254,18 @@
       val T = Term.fastype_of1 (Us @ Ts, t)
       val lev = length Us
       val bs = sort int_ord (Term.add_loose_bnos (t, lev, []))
-      val bss = map_index (fn (i, j) => (j, Integer.add lev i)) bs
+      val bss = map_index (fn (i, j) => (j + lev, i + lev)) bs
       val norm = perhaps (AList.lookup (op =) bss)
       val t' = Term.map_aterms (fn Bound i => Bound (norm i) | t => t) t
       val Ts' = map (nth Ts) bs
 
       fun mk_abs U u = Abs (Name.uu, U, u)
       val abs_rhs = fold mk_abs Ts' (fold mk_abs Us t')
+
+      fun app f = Term.list_comb (f, map Bound bs)
     in
       (case Termtab.lookup defs abs_rhs of
-        SOME (f, _) => (Term.list_comb (f, map Bound bs), cx)
+        SOME (f, _) => (app f, cx)
       | NONE =>
           let
             val (n, ctxt') =
@@ -275,7 +277,7 @@
               |> fold_rev (mk_bapp o snd) bss
               |> fold_rev mk_bapp (0 upto (length Us - 1))
             val def = mk_def (Us @ Ts') T lhs t'
-          in (f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end)
+          in (app f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end)
     end
 
   fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t