merged

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 04 09:00:10 2012 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 04 10:49:42 2012 +0200
@@ -1334,7 +1334,7 @@
       let
         val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
       in
-        if member (op =) (modes_of Pred ctxt predname) full_mode then
+        if member eq_mode  (modes_of Pred ctxt predname) full_mode then
           let
             val Ts = binder_types T
             val arg_names = Name.variant_list []

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 04 09:00:10 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 04 10:49:42 2012 +0200
@@ -363,6 +363,16 @@
             (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
               Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
       end
+      | eval_function (T as Type (@{type_name prod}, [fT, sT])) =
+        let
+          val (ft', fT') = eval_function fT
+          val (st', sT') = eval_function sT
+          val T' = Type (@{type_name prod}, [fT', sT'])
+          val map_const = Const (@{const_name map_pair}, (fT' --> fT) --> (sT' --> sT) --> T' --> T)
+          fun apply_dummy T t = absdummy T (t (Bound 0))
+        in
+          (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T')
+        end
       | eval_function T = (I, T)
     val (tt, boundTs') = split_list (map eval_function boundTs)
     val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t)