diff -r e77f2858bd59 -r aa41ecbdc205 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Thu Feb 13 11:37:00 2014 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Thu Feb 13 11:54:14 2014 +0100 @@ -79,7 +79,7 @@ replacing = [], manual_reorder = []}) *} -values 40 "{s. hotel s}" +values_prolog 40 "{s. hotel s}" setup {* Context.theory_map