# HG changeset patch
# User wenzelm
# Date 918148501 -3600
# Node ID 42c94393d39ed1c563683fb03ea20f15b229d6cc
# Parent  f453bd781dfd1008e99885d9c4531ebcb2a5fdd5
use, cd;

diff -r f453bd781dfd -r 42c94393d39e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Feb 04 18:14:40 1999 +0100
+++ b/src/Pure/ROOT.ML	Thu Feb 04 18:15:01 1999 +0100
@@ -73,6 +73,9 @@
 end;
 
 use "install_pp.ML";
-open BasicUse;
+
+val use = ThyInfo.load_file o Path.unpack;
+val cd = File.cd o Path.unpack;
+
 print_depth 8;
 (*ml_prompts "ML> " "ML# ";*)