* Result facts now refer to the *full* internal name;

--- a/NEWS	Tue Sep 02 20:04:26 2008 +0200
+++ b/NEWS	Tue Sep 02 20:07:51 2008 +0200
@@ -188,6 +188,10 @@
 user to underlying specification mechanisms; this enables precise
 tracking of source positions, for example.
 
+* Result facts (from PureThy.note_thms, ProofContext.note_thms,
+LocalTheory.note etc.) now refer to the *full* internal name, not the
+bstring as before.  INCOMPATIBILITY, not detected by ML type-checking!
+
 * Rules and tactics that read instantiations (read_instantiate,
 res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
 context, which is required for parsing and type-checking.  Moreover,