src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
changeset 39800 17e29ddd538e
parent 39463 7ce0ed8dc4d6
child 40301 bf39a257b3d3
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 30 10:48:12 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 30 10:48:12 2010 +0200
@@ -58,6 +58,7 @@
 
 setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = true,
+  limit_globally = NONE,
   limited_types = [],
   limited_predicates = [(["s1", "a1", "b1"], 2)],
   replacing = [(("s1", "limited_s1"), "quickcheck")],
@@ -81,6 +82,7 @@
 
 setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = true,
+  limit_globally = NONE,
   limited_types = [],
   limited_predicates = [(["s2", "a2", "b2"], 3)],
   replacing = [(("s2", "limited_s2"), "quickcheck")],
@@ -103,6 +105,7 @@
 
 setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = true,
+  limit_globally = NONE,
   limited_types = [],
   limited_predicates = [(["s3", "a3", "b3"], 6)],
   replacing = [(("s3", "limited_s3"), "quickcheck")],
@@ -117,6 +120,7 @@
 (*
 setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = true,
+  limit_globally = NONE,
   limited_types = [],
   limited_predicates = [],
   replacing = [],
@@ -143,6 +147,7 @@
 
 setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = true,
+  limit_globally = NONE,
   limited_types = [],
   limited_predicates = [(["s4", "a4", "b4"], 6)],
   replacing = [(("s4", "limited_s4"), "quickcheck")],