It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...

--- a/src/HOL/List.thy	Mon Sep 01 19:17:47 2008 +0200
+++ b/src/HOL/List.thy	Mon Sep 01 22:10:42 2008 +0200
@@ -3626,6 +3626,14 @@
 
 text {* Code for bounded quantification and summation over nats. *}
 
+lemma atMost_upto [code unfold]:
+  "{..n} = set [0..<Suc n]"
+by auto
+
+lemma atLeast_upt [code unfold]:
+  "{..<n} = set [0..<n]"
+by auto
+
 lemma greaterThanLessThan_upt [code unfold]:
   "{n<..<m} = set [Suc n..<m]"
 by auto