--- 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