# HG changeset patch
# User wenzelm
# Date 939162888 -7200
# Node ID 91d16d251ea72fa35190da17974e8ba5ab0da172
# Parent  e634168295388846ef2ff05d96259168f014845a
tuned comment;

diff -r e63416829538 -r 91d16d251ea7 src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Wed Oct 06 00:33:53 1999 +0200
+++ b/src/Pure/Thy/ROOT.ML	Wed Oct 06 00:34:48 1999 +0200
@@ -21,4 +21,5 @@
 use "latex.ML";
 use "present.ML";
 
+(*theorem database -- user-level interface*)
 use "thm_database.ML";