# HG changeset patch
# User berghofe
# Date 899311420 -7200
# Node ID 2edf5dfb02f322f6e0aa062c753d5d4dd38cabe0
# Parent  05b7c9a2ddf9022b2e68c8c8dcb53ec3bf639f68
Replaced "use_dir" command by "use", because nested calls
of "use_dir" cause the HTML generator to crash.

diff -r 05b7c9a2ddf9 -r 2edf5dfb02f3 src/HOL/ROOT.ML
--- 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";