diff -r dc2236b19a3d -r 74515e8e6046 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Nov 11 08:32:48 2011 +0100
@@ -93,8 +93,7 @@
 (*nitpick
 quickcheck[tester = random, iterations = 10000]
 quickcheck[tester = predicate_compile_wo_ff]
-quickcheck[tester = predicate_compile_ff_fs]
-oops*)
+quickcheck[tester = predicate_compile_ff_fs]*)
 oops
 
 
@@ -117,7 +116,8 @@
  prolog-style generation. *}
 
 lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-quickcheck[tester = random, iterations = 100000]
+quickcheck[exhaustive]
+quickcheck[tester = random, iterations = 1000]
 (*quickcheck[tester = predicate_compile_wo_ff]*)
 (*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
 (*quickcheck[tester = prolog, iterations = 1, size = 1]*)
@@ -170,13 +170,13 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
   assumes "s = [N0, N0]"
 shows "prop_regex (n, (k, (p, (q, s))))"
-quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = smart_exhaustive, depth = 30]
 quickcheck[tester = prolog]
 oops
 
 lemma "prop_regex a_sol"
 quickcheck[tester = random]
-quickcheck[tester = predicate_compile_ff_fs]
+quickcheck[tester = smart_exhaustive]
 oops
 
 value [code] "prop_regex a_sol"