# HG changeset patch
# User wenzelm
# Date 1213383847 -7200
# Node ID 0fe5b95797da97109c8b53dc6efaee81989b7dc4
# Parent  431f695fc86527612867ee61f04f439668b1aebe
* Recovered hiding of consts;

diff -r 431f695fc865 -r 0fe5b95797da NEWS
--- a/NEWS	Fri Jun 13 20:57:51 2008 +0200
+++ b/NEWS	Fri Jun 13 21:04:07 2008 +0200
@@ -6,6 +6,10 @@
 
 *** Pure ***
 
+* Recovered hiding of consts, which was accidentally broken in
+Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really
+makes c inaccessible; consider using ``hide (open) const c'' instead.
+
 * Command 'instance': attached definitions now longer accepted.
 INCOMPATIBILITY, use proper 'instantiation' target.