* ML in Isar: improved error reporting;

--- a/NEWS	Sun Jan 21 17:13:30 2007 +0100
+++ b/NEWS	Sun Jan 21 19:09:35 2007 +0100
@@ -771,6 +771,9 @@
 
 The same works for sources being ``used'' within an Isar context.
 
+* ML in Isar: improved error reporting; extra verbosity with
+Toplevel.debug enabled.
+
 * Pure/library:
 
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list