* Context-dependent token translations.

--- a/NEWS	Thu Apr 17 22:22:30 2008 +0200
+++ b/NEWS	Thu Apr 17 22:28:56 2008 +0200
@@ -34,6 +34,9 @@
 
 *** Pure ***
 
+* Context-dependent token translations.  Default setup reverts locally
+fixed variables, and adds hilite markup for undeclared frees.
+
 * Unused theorems can be found using the new command 'unused_thms'.
 There are three ways of invoking it:
 
@@ -49,16 +52,17 @@
      their ancestors, excluding the theories thy_1 ... thy_n and all of
      their ancestors.
 
-In order to increase the readability of the list produced by unused_thms,
-theorems that have been created by a particular instance of a theory
-command such as inductive or fun(ction) are considered to belong to the
-same "group", meaning that if at least one theorem in this group is used,
-the other theorems in the same group are no longer reported as unused.
-Moreover, if all theorems in the group are unused, only one theorem in
-the group is displayed.
-Note that proof objects have to be switched on in order for unused_thms
-to work properly (i.e. !proofs must be >= 1, which is usually the case
-when using ProofGeneral with the default settings).
+In order to increase the readability of the list produced by
+unused_thms, theorems that have been created by a particular instance
+of a theory command such as inductive or fun(ction) are considered to
+belong to the same "group", meaning that if at least one theorem in
+this group is used, the other theorems in the same group are no longer
+reported as unused.  Moreover, if all theorems in the group are
+unused, only one theorem in the group is displayed.
+
+Note that proof objects have to be switched on in order for
+unused_thms to work properly (i.e. !proofs must be >= 1, which is
+usually the case when using ProofGeneral with the default settings).
 
 * Authentic naming of facts disallows ad-hoc overwriting of previous
 theorems within the same name space.  INCOMPATIBILITY, need to remove