NEWS

 to emphasize that these only work in a global situation (which is
 quite rare).
 
 * Configuration options now admit dynamic default values, depending on
 the context or even global references.
+
+* Most operations that refer to a global context are named
+accordingly, e.g. Simplifier.global_context or
+ProofContext.init_global.  There are some situations where a global
+context actually works, but under normal circumstances one needs to
+pass the proper local context through the code!
 
 
 *** System ***
 
 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;