# HG changeset patch
# User wenzelm
# Date 1206398071 -3600
# Node ID 7807cbf7640f668469fb2013072959cd167d23c6
# Parent  9c806de22a6ae880b6e18676596a568f3ce71054
removed obsolete use_legacy_bindings;

diff -r 9c806de22a6a -r 7807cbf7640f NEWS
--- a/NEWS	Mon Mar 24 23:34:30 2008 +0100
+++ b/NEWS	Mon Mar 24 23:34:31 2008 +0100
@@ -172,6 +172,8 @@
 
 *** ML ***
 
+* Removed obsolete "use_legacy_bindings" function.  INCOMPATIBILITY.
+
 * ML within Isar: antiquotation @{const name} or @{const
 name(typargs)} produces statically-checked Const term.