# HG changeset patch
# User wenzelm
# Date 1178629288 -7200
# Node ID e1d3fa78b8e1681446a867865919083bdfb4ae57
# Parent  3dd306cb98d2b2dac078b8478fd7d03cfc04d378
tuned context data;

diff -r 3dd306cb98d2 -r e1d3fa78b8e1 NEWS
--- a/NEWS	Tue May 08 08:21:39 2007 +0200
+++ b/NEWS	Tue May 08 15:01:28 2007 +0200
@@ -903,8 +903,9 @@
 *** ML ***
 
 * Context data interfaces (Theory/Proof/GenericDataFun): removed
-name/print, use adhoc value for uninitialized data, init only required
-for impure data.
+name/print, uninitialized data defaults to ad-hoc copy of empty value,
+init only required for impure data.  INCOMPATIBILITY: empty really
+need to be empty (no dependencies on theory content!)
 
 * ML within Isar: antiquotations allow to embed statically-checked
 formal entities in the source, referring to the context available at