diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Computational_Algebra/Squarefree.thy
--- a/src/HOL/Computational_Algebra/Squarefree.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Squarefree.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -116,13 +116,16 @@
   show ?thesis unfolding squarefree_factorial_semiring'[OF nz]
   proof
     fix p assume p: "p \<in> prime_factors (a * b)"
-    {
+    with nz have "prime p"
+      by (simp add: prime_factors_dvd)
+    have "\<not> (p dvd a \<and> p dvd b)"
+    proof
       assume "p dvd a \<and> p dvd b"
-      hence "p dvd gcd a b" by simp
-      also have "gcd a b = 1" by fact
-      finally have False using nz using p by (auto simp: prime_factors_dvd)
-    }
-    hence "\<not>(p dvd a \<and> p dvd b)" by blast
+      with \<open>coprime a b\<close> have "is_unit p"
+        by (auto intro: coprime_common_divisor)
+      with \<open>prime p\<close> show False
+        by simp
+    qed
     moreover from p have "p dvd a \<or> p dvd b" using nz 
       by (auto simp: prime_factors_dvd prime_dvd_mult_iff)
     ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3)
@@ -138,7 +141,7 @@
   shows   "squarefree (prod f A)"
   using assms 
   by (induction A rule: infinite_finite_induct) 
-     (auto intro!: squarefree_mult_coprime prod_coprime')
+     (auto intro!: squarefree_mult_coprime prod_coprime_right)
 
 lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n"
   by (cases m) (auto dest: squarefree_multD)