diff -r b7d0e78be86d -r cd928fd965a8 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Thu May 31 18:16:46 2007 +0200
+++ b/src/FOL/ROOT.ML	Thu May 31 18:16:47 2007 +0200
@@ -1,10 +1,7 @@
 (*  Title:      FOL/ROOT.ML
     ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+
+First-Order Logic with Natural Deduction.
 *)
 
-val banner = "First-Order Logic with Natural Deduction";
-writeln banner;
-
 use_thy "FOL";