diff -r 3917c2acaec4 -r b5d126d7be4b src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Aug 31 15:07:51 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Aug 31 15:21:56 2010 +0200 @@ -10,8 +10,12 @@ "append [] ys ys" | "append xs ys zs ==> append (x # xs) ys (x # zs)" -setup {* Code_Prolog.map_code_options (K {ensure_groundness = false, - limited_types = [], limited_predicates = [], replacing = [], +setup {* Code_Prolog.map_code_options (K + {ensure_groundness = false, + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = [], prolog_system = Code_Prolog.SWI_PROLOG}) *} values "{(x, y, z). append x y z}" @@ -20,14 +24,20 @@ setup {* Code_Prolog.map_code_options (K {ensure_groundness = false, - limited_types = [], limited_predicates = [], replacing = [], + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = [], prolog_system = Code_Prolog.YAP}) *} values "{(x, y, z). append x y z}" setup {* Code_Prolog.map_code_options (K {ensure_groundness = false, - limited_types = [], limited_predicates = [], replacing = [], + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = [], prolog_system = Code_Prolog.SWI_PROLOG}) *} @@ -191,11 +201,13 @@ where "y \ B \ notB y" -setup {* Code_Prolog.map_code_options (K {ensure_groundness = true, - limited_types = [], - limited_predicates = [], - replacing = [], - prolog_system = Code_Prolog.SWI_PROLOG}) *} +setup {* Code_Prolog.map_code_options (K + {ensure_groundness = true, + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = [], + prolog_system = Code_Prolog.SWI_PROLOG}) *} values 2 "{y. notB y}"