1.1 --- a/src/Pure/ROOT.ML	Fri Dec 11 18:34:10 2020 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Mon Dec 14 15:04:10 2020 +0100
     1.3 @@ -102,9 +102,9 @@
     1.4  ML_file "name.ML";
     1.5  ML_file "term.ML";
     1.6  ML_file "context.ML";
     1.7 -(*ML \<open>@{print} {a = "..does NOT work up to here------------------------------------------//"}\<close>*)
     1.8 +(*ML \<open>@{print} {a = "..does NOT work up to here -----------------------------------------//"}\<close>*)
     1.9  ML_file "context_position.ML";
    1.10 -ML \<open>@{print} {a = "..works from here-----------------------------------------------------\\"}\<close>
    1.11 +(*ML \<open>@{print} {a = "..works from here, if ROOT.ML is loaded from some thy --------------\\"}\<close>*)
    1.12  ML_file "System/options.ML";
    1.13  ML_file "config.ML";
    1.14  ML_file "soft_type_system.ML";