# HG changeset patch
# User boehmes
# Date 1329605001 -3600
# Node ID a018d542e0ae5f82a226c5e6626a2b1f984b36e6
# Parent  1bbee2041321a10e8418c796d6c23ca513b1c224
corrected treatment of applications of built-in functions to higher-order terms

diff -r 1bbee2041321 -r a018d542e0ae src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Sat Feb 18 23:05:31 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Sat Feb 18 23:43:21 2012 +0100
@@ -228,6 +228,8 @@
               (case SMT_Builtin.dest_builtin ctxt c ts of
                 SOME (_, k, us, mk) =>
                   if k = length us then mk (map expand us)
+                  else if k < length us then
+                    chop k (map expand us) |>> mk |> Term.list_comb
                   else expf k (length ts) T (mk (map expand us))
               | NONE => exp_func u T (map expand ts))
           | (u as Free (_, T), ts) => exp_func u T (map expand ts)
@@ -299,7 +301,11 @@
           q $ traverse Ts u1 $ traverse Ts u2
       | (u as Const (c as (_, T)), ts) =>
           (case SMT_Builtin.dest_builtin ctxt c ts of
-            SOME (_, _, us, mk) => mk (map (traverse Ts) us)
+            SOME (_, k, us, mk) =>
+              let
+                val (ts1, ts2) = chop k (map (traverse Ts) us)
+                val U = Term.strip_type T |>> snd o chop k |> (op --->)
+              in apply 0 (mk ts1) U ts2 end
           | NONE => app_func u T (map (traverse Ts) ts))
       | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts)
       | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)