src/HOL/Numeral_Simprocs.thy

--- a/src/HOL/Numeral_Simprocs.thy	Tue Mar 27 14:49:56 2012 +0200
+++ b/src/HOL/Numeral_Simprocs.thy	Tue Mar 27 15:27:49 2012 +0200
@@ -72,7 +72,7 @@
 
 lemma nat_mult_dvd_cancel_disj[simp]:
   "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
-by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
+by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1)
 
 lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
 by(auto)