--- a/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 12:19:00 2010 +0000
+++ b/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 13:54:17 2010 +0100
@@ -202,7 +202,12 @@
fun expf t i T ts =
let val Ts = U.dest_funT i T |> fst |> drop (length ts)
- in Term.list_comb (t, ts) |> fold_rev eta Ts end
+ in
+ Term.list_comb (t, ts)
+ |> Term.incr_boundvars (length Ts)
+ |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
+ |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
+ end
fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
| expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
@@ -249,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') =
@@ -270,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
@@ -356,7 +363,7 @@
| (u as Bound i, ts) =>
appl0 (nth arities i) (map (traverse env) ts) (u, nth Ts i)
| (Abs (n, T, u), ts) =>
- let val env' = (get_arities 0 u [] :: arities, T :: Ts)
+ let val env' = (get_arities 0 u [0] :: arities, T :: Ts)
in traverses env (Abs (n, T, traverse env' u)) ts end
| (u, ts) => traverses env u ts)
and traverses env t ts = Term.list_comb (t, map (traverse env) ts)