# HG changeset patch
# User bulwahn
# Date 1310978061 -7200
# Node ID ee4be704c2a476239c85ed4a32bdd454a747046f
# Parent  442aceb54969fe94397e9ce2837a740a11cb038b
adapting an experimental setup to changes in quickcheck's infrastructure

diff -r 442aceb54969 -r ee4be704c2a4 src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Jul 18 10:34:21 2011 +0200
@@ -41,12 +41,19 @@
 
 end
 
-setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term
-  Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *}
+ML {* 
+val small_15_active = Attrib.setup_config_bool @{binding quickcheck_small_14_active} (K false);
+val small_14_active = Attrib.setup_config_bool @{binding quickcheck_small_15_active} (K false);
+*}
 
-
-setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term
-  Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *}
+setup {*
+  Context.theory_map (Quickcheck.add_tester ("small_generators_depth_14",
+    (small_14_active, Predicate_Compile_Quickcheck.test_goals
+      (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 14))))
+  #> Context.theory_map (Quickcheck.add_tester ("small_generators_depth_15",
+    (small_15_active, Predicate_Compile_Quickcheck.test_goals
+      (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 15))))
+*}
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
diff -r 442aceb54969 -r ee4be704c2a4 src/HOL/ex/Quickcheck_Lattice_Examples.thy
--- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Mon Jul 18 10:34:21 2011 +0200
@@ -18,6 +18,8 @@
   inf (infixl "\<sqinter>" 70) and
   sup (infixl "\<squnion>" 65)
 
+declare [[quickcheck_narrowing_active = false]]
+
 subsection {* Distributive lattices *}
 
 lemma sup_inf_distrib2: