changeset 6237 | 699b4daf1451 |
parent 6226 | 42c94393d39e |
child 6365 | 416c4679f937 |
--- a/src/Pure/ROOT.ML Fri Feb 05 17:31:42 1999 +0100 +++ b/src/Pure/ROOT.ML Fri Feb 05 20:56:50 1999 +0100 @@ -74,8 +74,10 @@ use "install_pp.ML"; -val use = ThyInfo.load_file o Path.unpack; +val use = ThyInfo.use; val cd = File.cd o Path.unpack; print_depth 8; (*ml_prompts "ML> " "ML# ";*) + +Session.finish ();