# HG changeset patch
# User wenzelm
# Date 1003766640 -7200
# Node ID 6b9e8820d4de518853887a23b339c516f264bb36
# Parent  4a8834757140084d06aa9f884805cb0799b081eb
tuned;

diff -r 4a8834757140 -r 6b9e8820d4de src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Mon Oct 22 18:03:49 2001 +0200
+++ b/src/Pure/Thy/ROOT.ML	Mon Oct 22 18:04:00 2001 +0200
@@ -22,5 +22,5 @@
 use "present.ML";
 use "thm_deps.ML";
 
-(*theorem database -- user-level interface*)
+(*theorem database interface*)
 use "thm_database.ML";