diff -r 075550af9e11 -r 4301eb0f051f src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Thu Feb 09 03:34:56 2006 +0100
+++ b/src/HOL/Integ/NatBin.thy	Thu Feb 09 12:14:39 2006 +0100
@@ -196,7 +196,10 @@
 
 subsubsection{* Divisibility *}
 
-declare dvd_eq_mod_eq_0[of "number_of x" "number_of y", standard, simp]
+lemmas dvd_eq_mod_eq_0_number_of =
+  dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
+
+declare dvd_eq_mod_eq_0_number_of [simp]
 
 ML
 {*