diff -r 59ba3dbd1400 -r 7caa1139b4e5 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Mon Jul 18 10:34:21 2011 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Mon Jul 18 10:34:21 2011 +0200 @@ -23,7 +23,7 @@ values 40 "{s. hotel s}" -setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} +setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *} lemma "\ hotel s; g \ isin s r \ \ owns s r = Some g" quickcheck[tester = random, iterations = 10000, report]