diff -r e3e6c83efc39 -r 3b5434efdf91 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 21:48:55 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 21:58:41 2012 +0200
@@ -172,11 +172,11 @@
 
 lemmas int_mod_eq' = refl [THEN [3] int_mod_eq]
 
-lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a"
-  by (rule zmod_le_nonneg_dividend)
+lemma int_mod_le: "(0::int) <= a ==> a mod n <= a"
+  by (fact zmod_le_nonneg_dividend) (* FIXME: delete *)
 
-lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n"
-  by (rule int_mod_le [where a = "b - n" and n = n, simplified])
+lemma int_mod_le': "(0::int) <= b - n ==> b mod n <= b - n"
+  using zmod_le_nonneg_dividend [of "b - n" "n"] by simp
 
 lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"
   apply (cases "0 <= a")