enter_thms: use theorem database of thy *after* attribute application;

--- a/src/Pure/pure_thy.ML	Tue Jun 21 09:35:32 2005 +0200
+++ b/src/Pure/pure_thy.ML	Tue Jun 21 09:51:59 2005 +0200
@@ -305,9 +305,9 @@
   | enter_thms pre_name post_name app_att (bname, thms) thy =
       let
         val name = Sign.full_name thy bname;
-        val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy;
-        val space' = Sign.declare_name thy name space;
         val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
+        val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy';
+        val space' = Sign.declare_name thy' name space;
         val theorems' = Symtab.update ((name, thms'), theorems);
         val index' = FactIndex.add (K false) (name, thms') index;
       in