# HG changeset patch
# User huffman
# Date 1313246375 25200
# Node ID 4a80017c733ff254053513f8636fbe8df2ee4ce6
# Parent  9411ed32f3a7ea646ac89c197888b01ac7088340
ex/Quickcheck_Examples.thy: respect distinction between sets and functions

diff -r 9411ed32f3a7 -r 4a80017c733f src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Sat Aug 13 12:23:51 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Sat Aug 13 07:39:35 2011 -0700
@@ -234,7 +234,7 @@
 oops
 
 lemma
-  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. {..<i} (length ys)]"
+  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
 quickcheck[random]
 quickcheck[exhaustive, expect = counterexample]
 oops