diff -r c143ad7811fc -r da1fdbfebd39 NEWS
--- a/NEWS	Tue Jul 30 12:07:14 2013 +0200
+++ b/NEWS	Tue Jul 30 15:09:25 2013 +0200
@@ -70,6 +70,12 @@
 
 *** Pure ***
 
+* Type theory is now immutable, without any special treatment of
+drafts or linear updates (which could lead to "stale theory" errors in
+the past).  Discontinued obsolete operations like Theory.copy,
+Theory.checkpoint, and the auxiliary type theory_ref.  Minor
+INCOMPATIBILITY.
+
 * System option "proofs" has been discontinued.  Instead the global
 state of Proofterm.proofs is persistently compiled into logic images
 as required, notably HOL-Proofs.  Users no longer need to change