src/Pure/ROOT.ML
changeset 6226 42c94393d39e
parent 6178 d6d6bdfe8340
child 6237 699b4daf1451
     1.1 --- a/src/Pure/ROOT.ML	Thu Feb 04 18:14:40 1999 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Feb 04 18:15:01 1999 +0100
     1.3 @@ -73,6 +73,9 @@
     1.4  end;
     1.5  
     1.6  use "install_pp.ML";
     1.7 -open BasicUse;
     1.8 +
     1.9 +val use = ThyInfo.load_file o Path.unpack;
    1.10 +val cd = File.cd o Path.unpack;
    1.11 +
    1.12  print_depth 8;
    1.13  (*ml_prompts "ML> " "ML# ";*)