Replaced "use_dir" command by "use", because nested calls
authorberghofe
Wed Jul 01 18:43:40 1998 +0200 (1998-07-01)
changeset 51072edf5dfb02f3
parent 5106 05b7c9a2ddf9
child 5108 4074c7d86d44
Replaced "use_dir" command by "use", because nested calls
of "use_dir" cause the HTML generator to crash.
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/ROOT.ML	Wed Jul 01 17:59:25 1998 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Wed Jul 01 18:43:40 1998 +0200
     1.3 @@ -56,7 +56,9 @@
     1.4  use_thy "Map";
     1.5  use_thy "Update";
     1.6  
     1.7 -use_dir "Integ";
     1.8 +cd "Integ";
     1.9 +use "ROOT.ML";
    1.10 +cd "..";
    1.11  
    1.12  (*TFL: recursive function definitions*)
    1.13  cd "$ISABELLE_HOME/src/TFL";