diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/Hahn_Banach/Zorn_Lemma.thy
--- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -31,13 +31,13 @@
     proof cases
 
       txt {* If @{text c} is an empty chain, then every element in
-	@{text S} is an upper bound of @{text c}. *}
+        @{text S} is an upper bound of @{text c}. *}
 
       assume "c = {}"
       with aS show ?thesis by fast
 
       txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper
-	bound of @{text c}, lying in @{text S}. *}
+        bound of @{text c}, lying in @{text S}. *}
 
     next
       assume "c \<noteq> {}"
@@ -47,7 +47,7 @@
         show "\<Union>c \<in> S"
         proof (rule r)
           from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast
-	  show "c \<in> chain S" by fact
+          show "c \<in> chain S" by fact
         qed
       qed
     qed