src/HOL/GCD.thy

       by blast
     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
       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)
     from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
     have "a' dvd b'" by (subst (asm) mult.commute, blast)