diff -r fcff6903595f -r f3c5da707f30 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 16 13:49:11 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 16 13:49:12 2010 +0200
@@ -19,6 +19,8 @@
 
 values "{(x, y, z). append x y z}"
 
+values 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}"
+
 values 3 "{(x, y, z). append x y z}"
 
 setup {* Code_Prolog.map_code_options (K