diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Fri Oct 01 16:05:25 2010 +0200
@@ -8,8 +8,8 @@
 imports Main Parity
 begin
 
-lemma contentsI: "y = {x} ==> contents y = x" 
-  unfolding contents_def by auto -- {* FIXME move *}
+lemma the_elemI: "y = {x} ==> the_elem y = x" 
+  by simp
 
 lemmas split_split = prod.split
 lemmas split_split_asm = prod.split_asm