author | wenzelm |
Wed, 06 Aug 1997 14:10:22 +0200 | |
changeset 3625 | 33f718b4f7bf |
parent 3624 | 36e19fce289e |
child 3626 | d91708377b6a |
--- 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 *)