NEWS

--- a/NEWS	Tue Mar 03 19:08:04 2015 +0100
+++ b/NEWS	Wed Mar 04 19:53:18 2015 +0100
@@ -258,6 +258,10 @@
 
 *** ML ***
 
+* Elementary operations in module Thm are no longer pervasive.
+INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,
+Thm.term_of etc.
+
 * Former combinators NAMED_CRITICAL and CRITICAL for central critical
 sections have been discontinued, in favour of the more elementary
 Multithreading.synchronized and its high-level derivative