diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Word/Word.thy	Thu Dec 10 13:38:40 2015 +0000
@@ -3599,7 +3599,7 @@
       apply (simp (no_asm), arith)
      apply (simp (no_asm), arith)
     apply (rule notI [THEN notnotD],
-           drule leI not_leE,
+           drule leI not_le_imp_less,
            drule sbintrunc_inc sbintrunc_dec,      
            simp)+
   done