# HG changeset patch
# User wenzelm
# Date 1220378871 -7200
# Node ID 66ae1926482ad57e9b34e6baa1bd5a21b919618b
# Parent  723735f2d73aa95411380aa81ee203077c306395
* Result facts now refer to the *full* internal name;

diff -r 723735f2d73a -r 66ae1926482a NEWS
--- 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,