diff -r 96a5f44c22da -r 8a070c62b548 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Dec 28 10:30:43 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Dec 28 10:48:39 2011 +0100
@@ -1072,9 +1072,7 @@
 subsection {* Word Arithmetic *}
 
 lemma word_less_alt: "(a < b) = (uint a < uint b)"
-  unfolding word_less_def word_le_def
-  by (auto simp del: word_uint.Rep_inject 
-           simp: word_uint.Rep_inject [symmetric])
+  unfolding word_less_def word_le_def by (simp add: less_le)
 
 lemma signed_linorder: "class.linorder word_sle word_sless"
 proof