# HG changeset patch
# User wenzelm
# Date 1425681891 -3600
# Node ID 34030d67afb9c937d049bf4f76fb342b35c377ea
# Parent  c9aa1c90796f5079e851ec4c1ae13fba40669876
clarified context;

diff -r c9aa1c90796f -r 34030d67afb9 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Mar 06 23:38:59 2015 +0100
+++ b/src/HOL/String.thy	Fri Mar 06 23:44:51 2015 +0100
@@ -248,7 +248,7 @@
 
 setup {*
 let
-  val nibbles = map_range (Thm.global_cterm_of @{theory} o HOLogic.mk_nibble) 16;
+  val nibbles = map_range (Thm.cterm_of @{context} o HOLogic.mk_nibble) 16;
   val simpset =
     put_simpset HOL_ss @{context}
       addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};