diff -r e5ba49a72ab9 -r adf3155c57e2 src/HOL/Predicate_Compile_Examples/Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Sun Jul 16 23:47:21 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Mon Jul 17 16:49:19 2017 +0200
@@ -311,14 +311,7 @@
 definition list :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list" where
   "list s n = map s [0 ..< n]"
 
-values [expected "{[Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
-     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
-     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
-     )))))))))))))))))))))))))))))))))))))))),
-   Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc   (Suc (Suc (Suc (Suc
-     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
-     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
-     )))))))))))))))))))))))))))))))))))))))))]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
+values [expected "{[42::nat, 43]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
 
 
 subsection \<open>CCS\<close>