(adjusted)

--- a/doc-src/TutorialI/Rules/Primes.thy	Sat Jul 19 19:27:13 2008 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Sun Jul 20 11:10:04 2008 +0200
@@ -151,7 +151,7 @@
 
 
 lemma gcd_dvd_gcd_mult: "gcd m n dvd gcd (k*m) n"
-  apply (blast intro: dvd_trans);
+  apply (auto intro: dvd_trans [of _ m])
   done
 
 (*This is half of the proof (by dvd_anti_sym) of*)