# HG changeset patch
# User bulwahn
# Date 1284637752 -7200
# Node ID f3c5da707f3089de046f3a2b735351a4509a24b7
# Parent  fcff6903595f1cc58414085715ba2731b9e3c34c
adding values to show and ensure that values works with complex terms and restores numerals on natural numbers

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