New reference Toplevel.debug for verbose printing of exns.

--- a/NEWS	Fri Feb 11 04:36:22 2005 +0100
+++ b/NEWS	Fri Feb 11 10:03:41 2005 +0100
@@ -178,6 +178,9 @@
 
 *** Isar ***
 
+* Debugging: new reference Toplevel.debug; default false.
+  Set to make printing of exceptions THM, TERM, TYPE and THEORY more verbose.
+  
 * Locales:
   - "includes" disallowed in declaration of named locales (command "locale").
   - Fixed parameter management in theorem generation for goals with "includes".