src/HOL/String.thy
changeset 59621 291934bac95e
parent 59484 a130ae7a9398
child 59631 34030d67afb9
     1.1 --- a/src/HOL/String.thy	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/String.thy	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -248,7 +248,7 @@
     1.4  
     1.5  setup {*
     1.6  let
     1.7 -  val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
     1.8 +  val nibbles = map_range (Thm.global_cterm_of @{theory} o HOLogic.mk_nibble) 16;
     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};