# HG changeset patch
# User wenzelm
# Date 870869422 -7200
# Node ID 33f718b4f7bf5cdac90ec14e31f56acecbeac6e1
# Parent  36e19fce289ea79c5843390440b0636c3bb084bf
ThmDatabase;

diff -r 36e19fce289e -r 33f718b4f7bf src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Wed Aug 06 14:09:50 1997 +0200
+++ b/src/Pure/Thy/ROOT.ML	Wed Aug 06 14:10:22 1997 +0200
@@ -17,7 +17,7 @@
 use "symbol_input.ML";
 use "thy_read.ML";
 
-open ThmDB ThyRead ThyInfo BrowserInfo SymbolInput;
+open ThmDatabase ThyRead ThyInfo BrowserInfo SymbolInput;
 
 
 (* FIXME tmp *)