--- 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";