diff -r 771117253634 -r 25ca91279a9b src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Library/GCD.thy	Wed Jun 20 05:18:39 2007 +0200
@@ -265,7 +265,7 @@
   from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
     unfolding dvd_def by blast
   from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
-  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by simp
+  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
   then show ?thesis
     apply (subst zdvd_abs1 [symmetric])
     apply (subst zdvd_abs2 [symmetric])