--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sun Sep 06 22:14:51 2015 +0200
@@ -316,7 +316,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
+ (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
fun mk_scomp_split T t t' =
mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
(mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
@@ -362,7 +362,7 @@
fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
fun mk_split T = Sign.mk_const thy
- (@{const_name case_prod}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
+ (@{const_name uncurry}, [T, @{typ "unit => term"}, liftT resultT @{typ Random.seed}]);
fun mk_scomp_split T t t' =
mk_scomp (mk_termtyp T) resultT @{typ Random.seed} t
(mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));