src/HOL/String.thy

--- a/src/HOL/String.thy	Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/String.thy	Thu Oct 22 13:48:06 2009 +0200
@@ -48,7 +48,7 @@
 
 setup {*
 let
-  val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
+  val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
   val thms = map_product
    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
       nibbles nibbles;