diff -r e08a0855af67 -r fcb507c945c3 src/HOL/Library/ROOT.ML
--- a/src/HOL/Library/ROOT.ML	Thu May 31 16:52:47 2001 +0200
+++ b/src/HOL/Library/ROOT.ML	Thu May 31 16:52:54 2001 +0200
@@ -1,2 +1,1 @@
-
 use_thy "Library";