diff -r 23a8c5ac35f8 -r 69916a850301 src/FOL/ex/Classical.thy
--- a/src/FOL/ex/Classical.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/FOL/ex/Classical.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -418,7 +418,7 @@
 by fast
 
 text{*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
-	author U. Egly*}
+  author U. Egly*}
 lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->                
    (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z)))))                   
   &