--- a/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 16:27:32 2009 +0200
@@ -24,11 +24,11 @@
lemmas [code del] = char.recs char.cases char.size
-lemma [code, code_inline]:
+lemma [code, code_unfold]:
"char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)
-lemma [code, code_inline]:
+lemma [code, code_unfold]:
"char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)