diff -r 7ca8810b1d48 -r 5407bc278c9a src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Apr 13 13:24:27 2017 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Apr 13 10:10:06 2017 +0200
@@ -104,12 +104,12 @@
 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
 where
   "apply f a d =
-     (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs =>
-       case a (d - 1) of Narrowing_cons ta cas =>
+     (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs \<Rightarrow>
+       case a (d - 1) of Narrowing_cons ta cas \<Rightarrow>
        let
-         shallow = (d > 0 \<and> non_empty ta);
-         cs = [(\<lambda>xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
-       in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
+         shallow = d > 0 \<and> non_empty ta;
+         cs = [(\<lambda>(x # xs) \<Rightarrow> cf xs (conv cas x)). shallow, cf \<leftarrow> cfs]
+       in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p \<leftarrow> ps]) cs)"
 
 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
 where