--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 30 10:48:12 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 30 10:48:12 2010 +0200
@@ -12,6 +12,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -25,6 +26,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -34,6 +36,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -202,6 +205,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
--- 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")],
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 30 10:48:12 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 30 10:48:12 2010 +0200
@@ -83,6 +83,7 @@
setup {* Code_Prolog.map_code_options (K
{ ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
replacing = [(("typing", "limited_typing"), "quickcheck"),
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 30 10:48:12 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 30 10:48:12 2010 +0200
@@ -6,6 +6,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
limited_predicates = [(["appendP"], 4), (["revP"], 4)],
replacing =
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 30 10:48:12 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 30 10:48:12 2010 +0200
@@ -100,6 +100,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
(["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],