src/HOL/GCD.thy

--- a/src/HOL/GCD.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/GCD.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -1199,7 +1199,7 @@
           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
             by simp
           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
-            by (simp only: mult_assoc right_distrib)
+            by (simp only: mult_assoc distrib_left)
           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
             by algebra
           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp