diff -r 64a19ea435fc -r 83caa4f4bd56 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Dec 28 22:08:44 2011 +0100
+++ b/src/HOL/Divides.thy	Thu Dec 29 10:47:54 2011 +0100
@@ -2418,7 +2418,7 @@
 
 lemma one_div_nat_number_of [simp]:
      "Suc 0 div number_of v' = nat (1 div number_of v')" 
-by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
+  by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
 
 lemma mod_nat_number_of [simp]:
      "(number_of v :: nat)  mod  number_of v' =  
@@ -2432,7 +2432,7 @@
      "Suc 0 mod number_of v' =  
         (if neg (number_of v' :: int) then Suc 0
          else nat (1 mod number_of v'))"
-by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
+by (simp del: semiring_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric] semiring_numeral_1_eq_1 [symmetric]) 
 
 lemmas dvd_eq_mod_eq_0_number_of [simp] =
   dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y