--- a/src/HOL/Quickcheck.thy Tue Mar 29 23:46:46 2011 +0200
+++ b/src/HOL/Quickcheck.thy Wed Mar 30 09:44:16 2011 +0200
@@ -209,5 +209,12 @@
hide_type (open) randompred
hide_const (open) random collapse beyond random_fun_aux random_fun_lift
iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
+declare [[quickcheck_timing]]
+lemma
+ "rev xs = xs"
+quickcheck[tester = random, finite_types = true, report = false]
+
+quickcheck[tester = random, finite_types = false, report = false]
+oops
end