diff -r 1f980bbc6ad8 -r 59dd6be5834c src/HOL/ex/Predicate_Compile_Quickcheck.thy
--- a/src/HOL/ex/Predicate_Compile_Quickcheck.thy	Tue Mar 02 22:13:32 2010 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy	Tue Mar 02 22:13:33 2010 +0100
@@ -7,9 +7,9 @@
 uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
 begin
 
-setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false) *}
+setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 8) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 8) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 8) *}
 
 (*
 datatype alphabet = a | b