# HG changeset patch
# User wenzelm
# Date 1119132461 -7200
# Node ID 051db5bb21b599c61833033abe6fa8dff8f4e1d5
# Parent  7e27422c603edebb0518388b7d9ca8d8d63cb42b
improved comment;

diff -r 7e27422c603e -r 051db5bb21b5 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Sun Jun 19 00:02:06 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Sun Jun 19 00:07:41 2005 +0200
@@ -12,6 +12,9 @@
 > val ml_system = "mosml";
 > use "ML-Systems/mosml.ML";
 > use "ROOT.ML";
+> Session.finish ();
+> cd "../HOL";
+> use "ROOT.ML";
 *)
 
 (** ML system related **)