diff -r 98acc234d683 -r 6d28bbd33e2c src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Code_Numeral.thy	Tue Jul 14 16:27:32 2009 +0200
@@ -176,13 +176,13 @@
 
 end
 
-lemma zero_code_numeral_code [code_inline, code]:
+lemma zero_code_numeral_code [code, code_unfold]:
   "(0\<Colon>code_numeral) = Numeral0"
   by (simp add: number_of_code_numeral_def Pls_def)
 lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
   using zero_code_numeral_code ..
 
-lemma one_code_numeral_code [code_inline, code]:
+lemma one_code_numeral_code [code, code_unfold]:
   "(1\<Colon>code_numeral) = Numeral1"
   by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
 lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"