diff -r 4d0878d54ca5 -r 501b9bbd0d6e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Mar 30 10:41:27 2012 +0200
+++ b/src/HOL/Divides.thy	Fri Mar 30 11:16:35 2012 +0200
@@ -1086,7 +1086,7 @@
   by (simp add: numeral_2_eq_2 le_mod_geq)
 
 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
-by (simp add: nat_mult_2 [symmetric])
+by (simp add: mult_2 [symmetric])
 
 lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
 proof -