diff -r 075550af9e11 -r 4301eb0f051f src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Thu Feb 09 03:34:56 2006 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Thu Feb 09 12:14:39 2006 +0100
@@ -1047,7 +1047,10 @@
 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
 by(simp add:dvd_def zmod_eq_0_iff)
 
-declare zdvd_iff_zmod_eq_0[of "number_of x" "number_of y", standard, simp]
+lemmas zdvd_iff_zmod_eq_0_number_of =
+  zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
+
+declare zdvd_iff_zmod_eq_0_number_of [simp]
 
 lemma zdvd_0_right [iff]: "(m::int) dvd 0"
 by (simp add: dvd_def)