src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 34962 807f6ce0273d
parent 34028 1e6206763036
child 34963 366a1a44aac2
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 13:39:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 16:56:51 2010 +0100
     1.3 @@ -2562,9 +2562,9 @@
     1.4      val t_eval = if null outargs then t_pred else
     1.5        let
     1.6          val outargs_bounds = map (fn Bound i => i) outargs;
     1.7 -        val outargsTs = map (nth Ts) outargs_bounds;
     1.8 +        val outargsTs = map (fn i => nth Ts (length Ts - i - 1)) outargs_bounds;
     1.9          val T_pred = HOLogic.mk_tupleT outargsTs;
    1.10 -        val T_compr = HOLogic.mk_ptupleT fp (rev Ts);
    1.11 +        val T_compr = HOLogic.mk_ptupleT fp Ts;
    1.12          val k = length outargs - 1;
    1.13          val arrange_bounds = map_index (fn (i, j) => (k-i, k-j)) outargs_bounds
    1.14            |> sort (prod_ord (K EQUAL) int_ord)