enter_thms: use theorem database of thy *after* attribute application;
authorwenzelm
Tue Jun 21 09:51:59 2005 +0200 (2005-06-21)
changeset 16513f38693aad717
parent 16512 1fa048f2a590
child 16514 090c6a98c704
enter_thms: use theorem database of thy *after* attribute application;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Tue Jun 21 09:35:32 2005 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Jun 21 09:51:59 2005 +0200
     1.3 @@ -305,9 +305,9 @@
     1.4    | enter_thms pre_name post_name app_att (bname, thms) thy =
     1.5        let
     1.6          val name = Sign.full_name thy bname;
     1.7 -        val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy;
     1.8 -        val space' = Sign.declare_name thy name space;
     1.9          val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
    1.10 +        val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy';
    1.11 +        val space' = Sign.declare_name thy' name space;
    1.12          val theorems' = Symtab.update ((name, thms'), theorems);
    1.13          val index' = FactIndex.add (K false) (name, thms') index;
    1.14        in