--- a/doc-src/Ref/theories.tex Tue Jan 23 14:25:55 1996 +0100
+++ b/doc-src/Ref/theories.tex Fri Jan 26 12:45:09 1996 +0100
@@ -484,6 +484,17 @@
make
\end{ttbox}
+When using ML databases made this way to load additional theories or
+derive other databases from them, you have to be aware that HTML
+generation remains activated.
+
+The reason is that the boolean reference variable {\tt make_html} (see
+below) is set. Therefore HTML files are generated unless you assign a
+value of {\tt false} to {\tt make_html}. The only place where the
+environment variable {\tt MAKE_HTML} is used is in the makefile where
+it determines the initial value of {\tt make_html} for a newly made
+database.
+
As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
{\tt FOL}) and because the HTML files list a theory's ancestors, you
should not make HTML files for a logic if the HTML files for the base