diff -r ef1e0cb80fde -r 949d93804740 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Tue May 22 14:12:15 2018 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Tue May 22 11:08:37 2018 +0200
@@ -186,7 +186,7 @@
 oops
 
 lemma
-  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
+  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) (filter (\<lambda>ys. i < length ys) xs)"
 quickcheck[random, iterations = 10000]
 quickcheck[exhaustive, expect = counterexample]
 oops
@@ -228,13 +228,13 @@
 oops
 
 lemma
-  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
+  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. i < length ys) (remdups xs))"
 quickcheck[random]
 quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
-  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
+  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. length ys \<in> {..<i}) (List.transpose xs))"
 quickcheck[random]
 quickcheck[exhaustive, expect = counterexample]
 oops