tuned;

--- a/src/HOL/Library/Infinite_Set.thy	Wed Dec 28 23:24:18 2016 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Wed Dec 28 23:42:35 2016 +0100
@@ -152,7 +152,7 @@
   by (simp add: eventually_frequently)
 
 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
-  by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
+  by (simp add: cofinite_eq_sequentially)
 
 lemma
   shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
@@ -317,7 +317,7 @@
 proof (induction A)
   case (insert a A)
   with R show ?case
-    by (metis empty_iff insert_iff) 
+    by (metis empty_iff insert_iff)
 qed simp
 
 corollary Union_maximal_sets: