src/HOL/String.thy
changeset 33063 4d462963a7db
parent 32069 6d28bbd33e2c
child 33237 565ad811db21
     1.1 --- a/src/HOL/String.thy	Thu Oct 22 10:52:07 2009 +0200
     1.2 +++ b/src/HOL/String.thy	Thu Oct 22 13:48:06 2009 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  setup {*
     1.6  let
     1.7 -  val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
     1.8 +  val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
     1.9    val thms = map_product
    1.10     (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    1.11        nibbles nibbles;