diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Char_nat.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -54,7 +54,7 @@
   "nibble_of_nat (n mod 16) = nibble_of_nat n"
   unfolding nibble_of_nat_def Let_def by auto
 
-lemmas [code func] = nibble_of_nat_norm [symmetric]
+lemmas [code] = nibble_of_nat_norm [symmetric]
 
 lemma nibble_of_nat_simps [simp]:
   "nibble_of_nat  0 = Nibble0"
@@ -75,7 +75,7 @@
   "nibble_of_nat 15 = NibbleF"
   unfolding nibble_of_nat_def Let_def by auto
 
-lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
+lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
   [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
 
 lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
@@ -115,7 +115,7 @@
   nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
   "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
 
-lemma nibble_of_pair [code func]:
+lemma nibble_of_pair [code]:
   "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
   unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..