# HG changeset patch
# User wenzelm
# Date 1257710468 -3600
# Node ID d4e5f6a407795646e52110d3e72674e03c5731c3
# Parent  1a989c0b80d0353c0710e4c30711de19b7cebdc0# Parent  a08e6c1cbc049574df6cc7e8205755df01f9a91b
merged

diff -r a08e6c1cbc04 -r d4e5f6a40779 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 21:00:05 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 21:01:08 2009 +0100
@@ -2553,13 +2553,17 @@
         val outargs_bounds = map (fn Bound i => i) outargs;
         val outargsTs = map (nth Ts) outargs_bounds;
         val T_pred = HOLogic.mk_tupleT outargsTs;
-        val T_compr = HOLogic.mk_ptupleT fp Ts;
-        val arrange_bounds = map_index I outargs_bounds
+        val T_compr = HOLogic.mk_ptupleT fp (rev Ts);
+        val k = length outargs - 1;
+        val arrange_bounds = map_index (fn (i, j) => (k-i, k-j)) outargs_bounds
           |> sort (prod_ord (K EQUAL) int_ord)
           |> map fst;
-        val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split
-          (Term.list_abs (map (pair "") outargsTs,
-            HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)))
+        val (outargsTs', outargsT) = split_last outargsTs;
+        val (arrange, _) = fold_rev (fn U => fn (t, T) =>
+            (HOLogic.split_const (U, T, T_compr) $ Abs ("", U, t),
+             HOLogic.mk_prodT (U, T)))
+          outargsTs' (Abs ("", outargsT,
+            HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)), outargsT)
       in mk_map compfuns T_pred T_compr arrange t_pred end
   in t_eval end;