indexing literal facts: exclude background context;

--- a/NEWS	Wed Mar 05 21:24:06 2008 +0100
+++ b/NEWS	Wed Mar 05 21:24:07 2008 +0100
@@ -31,6 +31,12 @@
 See HOL/Complex/Complex.thy for an Isar example and
 HOL/Library/Eval.thy for an ML example.
 
+* Indexing of literal facts: be more serious about including only
+facts from the visible specification/proof context, but not the
+background context (locale etc.).  Affects `prop` notation and method
+"fact".  INCOMPATIBILITY: need to name facts explicitly in rare
+situations.
+
 
 *** HOL ***