diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/GCD.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -870,7 +870,8 @@
       by (simp add: ab'(1,2)[symmetric])
     hence "?g^n*a'^n dvd ?g^n *b'^n"
       by (simp only: power_mult_distrib mult.commute)
-    with zn z n have th0:"a'^n dvd b'^n" by auto
+    then have th0: "a'^n dvd b'^n"
+      using zn by auto
     have "a' dvd a'^n" by (simp add: m)
     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)