src/HOL/Word/Word.thy

--- a/src/HOL/Word/Word.thy	Wed Dec 28 22:08:44 2011 +0100
+++ b/src/HOL/Word/Word.thy	Thu Dec 29 10:47:54 2011 +0100
@@ -507,10 +507,12 @@
 
 lemmas td_sint = word_sint.td
 
-lemma word_number_of_alt [code_unfold_post]:
+lemma word_number_of_alt:
   "number_of b = word_of_int (number_of b)"
   by (simp add: number_of_eq word_number_of_def)
 
+declare word_number_of_alt [symmetric, code_abbrev]
+
 lemma word_no_wi: "number_of = word_of_int"
   by (auto simp: word_number_of_def)