do not open Legacy by default;
authorwenzelm
Tue, 18 May 2010 00:01:03 +0200
changeset 36961 7b14afc02fc4
parent 36960 01594f816e3a
child 36972 aa4bc5a4be1d
do not open Legacy by default;
NEWS
src/Pure/ROOT.ML
--- a/NEWS	Mon May 17 23:54:15 2010 +0200
+++ b/NEWS	Tue May 18 00:01:03 2010 +0200
@@ -502,8 +502,8 @@
 context actually works, but under normal circumstances one needs to
 pass the proper local context through the code!
 
-* Renamed some important ML structures, while keeping the old names as
-legacy aliases for some time:
+* Renamed some important ML structures, while keeping the old names
+for some time as aliases within the structure Legacy:
 
   OuterKeyword  ~>  Keyword
   OuterLex      ~>  Token
@@ -511,6 +511,9 @@
   OuterSyntax   ~>  Outer_Syntax
   SpecParse     ~>  Parse_Spec
 
+Note that "open Legacy" simplifies porting of sources, but forgetting
+to remove it again will complicate porting again in the future.
+
 
 *** System ***
 
--- a/src/Pure/ROOT.ML	Mon May 17 23:54:15 2010 +0200
+++ b/src/Pure/ROOT.ML	Tue May 18 00:01:03 2010 +0200
@@ -312,4 +312,3 @@
 
 end;
 
-open Legacy;  (* FIXME *)