# HG changeset patch
# User bulwahn
# Date 1290422109 -3600
# Node ID 5ccfc3ee7fe6f87d17ea04dc5052d85ef0da34ca
# Parent  58a6ba7ccfc597a979a5017e05c321e7d1dd36a0
adapting example in Predicate_Compile_Examples

diff -r 58a6ba7ccfc5 -r 5ccfc3ee7fe6 src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Nov 22 11:35:07 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Nov 22 11:35:09 2010 +0100
@@ -50,8 +50,8 @@
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = small_generators_depth_14, iterations = 1, size = 1, expect = no_counterexample]
-quickcheck[generator = small_generators_depth_15, iterations = 1, size = 1, expect = counterexample]
+quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample]
+quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample]
 oops