src/HOL/Number_Theory/Factorial_Ring.thy

   shows   "\<exists>b. b dvd a \<and> is_prime b"
 proof -
   from prime_factorization_exists'[OF assms(1)] guess A . note A = this
   moreover from A and assms have "A \<noteq> {#}" by auto
   then obtain x where "x \<in># A" by blast
-  with A(1) have "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod)
-  moreover from this A have "x dvd a" by simp
-  ultimately show ?thesis by blast
+  with A(1) have *: "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod)
+  with A have "x dvd a" by simp
+  with * show ?thesis by blast
 qed
 
 lemma prime_divisors_induct [case_names zero unit factor]:
   assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. is_prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
   shows   "P x"