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