src/HOL/String.thy
changeset 51717 9e7d1c139569
parent 51160 599ff65b85e2
child 52365 95186e6e4bf4
     1.1 --- a/src/HOL/String.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/String.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -252,8 +252,9 @@
     1.4  setup {*
     1.5  let
     1.6    val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
     1.7 -  val simpset = HOL_ss addsimps
     1.8 -    @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
     1.9 +  val simpset =
    1.10 +    put_simpset HOL_ss @{context}
    1.11 +      addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
    1.12    fun mk_code_eqn x y =
    1.13      Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
    1.14      |> simplify simpset;