diff -r 101ce92333f4 -r 1bd4b6d1c482 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
@@ -30,13 +30,24 @@
 oops
 
 lemma "rev xs = xs"
-  quickcheck[tester = narrowing, finite_types = false, default_type = int]
+  quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
 oops
 
 lemma "rev xs = xs"
+  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
+oops
+
+subsection {* Simple examples with functions *}
+
+declare [[quickcheck_finite_functions]]
+
+lemma "map f xs = map g xs"
   quickcheck[tester = narrowing, finite_types = true]
 oops
 
+lemma "map f xs = map f ys ==> xs = ys"
+  quickcheck[tester = narrowing, finite_types = true]
+oops
 
 subsection {* AVL Trees *}