--- a/src/HOL/Library/Formal_Power_Series.thy Thu Jul 21 10:52:27 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Jul 22 08:02:37 2016 +0200
@@ -1512,7 +1512,7 @@
assume "Lcm A \<noteq> 0"
from unbounded obtain f where f: "f \<in> A" "subdegree (Lcm A) < subdegree f"
unfolding bdd_above_def by (auto simp: not_le)
- moreover from this and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)"
+ moreover from f and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)"
by (intro dvd_imp_subdegree_le dvd_Lcm) simp_all
ultimately show False by simp
qed