NEWS
changeset 37216 3165bc303f66
parent 37158 c96e119b7fe9
child 37218 ffd587207d5d
--- a/NEWS	Mon May 31 19:36:13 2010 +0200
+++ b/NEWS	Mon May 31 21:06:57 2010 +0200
@@ -503,9 +503,12 @@
   OuterLex      ~>  Token
   OuterParse    ~>  Parse
   OuterSyntax   ~>  Outer_Syntax
+  PrintMode     ~>  Print_Mode
   SpecParse     ~>  Parse_Spec
+  ThyInfo       ~>  Thy_Info
+  ThyLoad       ~>  Thy_Load
+  ThyOutput     ~>  Thy_Output
   TypeInfer     ~>  Type_Infer
-  PrintMode     ~>  Print_Mode
 
 Note that "open Legacy" simplifies porting of sources, but forgetting
 to remove it again will complicate porting again in the future.