src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 55932 68c5104d2204
parent 55757 9fc71814b8c1
child 56135 efa24d31e595
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 06 13:36:15 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 06 13:36:48 2014 +0100
@@ -366,7 +366,7 @@
           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)
+          val map_const = Const (@{const_name map_prod}, (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')