Replaced "use_dir" command by "use", because nested calls
of "use_dir" cause the HTML generator to crash.

--- a/src/HOL/ROOT.ML	Wed Jul 01 17:59:25 1998 +0200
+++ b/src/HOL/ROOT.ML	Wed Jul 01 18:43:40 1998 +0200
@@ -56,7 +56,9 @@
 use_thy "Map";
 use_thy "Update";
 
-use_dir "Integ";
+cd "Integ";
+use "ROOT.ML";
+cd "..";
 
 (*TFL: recursive function definitions*)
 cd "$ISABELLE_HOME/src/TFL";