tuned

--- a/NEWS	Wed Dec 12 09:00:07 2007 +0100
+++ b/NEWS	Wed Dec 12 19:26:37 2007 +0100
@@ -28,6 +28,8 @@
 definition/function/....  No separate induction rule is provided.
 The "primrec" command distinguishes old-style and new-style specifications
 by syntax.  The former primrec package is now named OldPrimrecPackage.
+When adjusting theories, beware: constants stemming for new-style
+primrec specifications have authentic syntax.
 
 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.