author | wenzelm |
Fri, 05 Feb 1999 20:56:50 +0100 | |
changeset 6237 | 699b4daf1451 |
parent 6236 | 958f4fc3e8b8 |
child 6238 | bd7b4a23118f |
src/Pure/ROOT.ML | file | annotate | diff | comparison | revisions |
--- 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 ();