
diff -r 5ab54bf226ac -r 6ceb8d38bc9e src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -169,13 +169,13 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
   assumes "s = [N0, N0]"
 shows "prop_regex (n, (k, (p, (q, s))))"
-quickcheck[generator = predicate_compile_wo_ff, expect = counterexample]
+quickcheck[generator = predicate_compile_wo_ff]
 quickcheck[generator = prolog, expect = counterexample]
 oops
 
 lemma "prop_regex a_sol"
 quickcheck[generator = code, expect = counterexample]
-quickcheck[generator = predicate_compile_ff_fs, expect = counterexample]
+quickcheck[generator = predicate_compile_ff_fs]
 oops
 
 value [code] "prop_regex a_sol"




