diff -r 3aa9837d05c7 -r 9c0ff0c12116 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sun Oct 02 14:07:43 2016 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Sun Oct 02 14:37:50 2016 +0200
@@ -331,7 +331,7 @@
     assume "S \<in> \<F>"
     have "{T \<in> \<F>. S \<subseteq> T} = {}" if "~ (\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y)"
       apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"])
-	 using assms that apply auto
+      using assms that apply auto
       by (blast intro: dual_order.trans psubset_imp_subset)
     then show "\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y"
       using \<open>S \<in> \<F>\<close> by blast