1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 12:33:06 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 16 13:34:28 2010 +0100
     1.3 @@ -254,16 +254,18 @@
     1.4        val T = Term.fastype_of1 (Us @ Ts, t)
     1.5        val lev = length Us
     1.6        val bs = sort int_ord (Term.add_loose_bnos (t, lev, []))
     1.7 -      val bss = map_index (fn (i, j) => (j, Integer.add lev i)) bs
     1.8 +      val bss = map_index (fn (i, j) => (j + lev, i + lev)) bs
     1.9        val norm = perhaps (AList.lookup (op =) bss)
    1.10        val t' = Term.map_aterms (fn Bound i => Bound (norm i) | t => t) t
    1.11        val Ts' = map (nth Ts) bs
    1.12  
    1.13        fun mk_abs U u = Abs (Name.uu, U, u)
    1.14        val abs_rhs = fold mk_abs Ts' (fold mk_abs Us t')
    1.15 +
    1.16 +      fun app f = Term.list_comb (f, map Bound bs)
    1.17      in
    1.18        (case Termtab.lookup defs abs_rhs of
    1.19 -        SOME (f, _) => (Term.list_comb (f, map Bound bs), cx)
    1.20 +        SOME (f, _) => (app f, cx)
    1.21        | NONE =>
    1.22            let
    1.23              val (n, ctxt') =
    1.24 @@ -275,7 +277,7 @@
    1.25                |> fold_rev (mk_bapp o snd) bss
    1.26                |> fold_rev mk_bapp (0 upto (length Us - 1))
    1.27              val def = mk_def (Us @ Ts') T lhs t'
    1.28 -          in (f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end)
    1.29 +          in (app f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end)
    1.30      end
    1.31  
    1.32    fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t