diff -r a303daddebbf -r d325c7c4a4f7 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Dec 23 14:24:21 2013 +0100
+++ b/src/HOL/Word/Word.thy	Mon Dec 23 14:24:22 2013 +0100
@@ -4010,9 +4010,6 @@
 
 subsubsection "map, map2, commuting with rotate(r)"
 
-lemma last_map: "xs ~= [] \<Longrightarrow> last (map f xs) = f (last xs)"
-  by (induct xs) auto
-
 lemma butlast_map:
   "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
   by (induct xs) auto