# HG changeset patch
# User berghofe
# Date 1257691509 -3600
# Node ID 05c384cb11819a3f0a33812f01ef3da1cccdd981
# Parent  771ec7306438f320fba02f5d716403ae699a99d0
Repaired handling of comprehensions in "values" command.

diff -r 771ec7306438 -r 05c384cb1181 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 13:44:16 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 15:45:09 2009 +0100
@@ -2554,13 +2554,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;