src/Pure/Isar/attrib.ML
changeset 42375 774df7c59508
parent 42360 da8817d01e7c
child 42380 9371ea9f91fb
     1.1 --- a/src/Pure/Isar/attrib.ML	Sun Apr 17 13:47:22 2011 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sun Apr 17 19:54:04 2011 +0200
     1.3 @@ -83,7 +83,9 @@
     1.4    end;
     1.5  
     1.6  fun add_attribute name att comment thy = thy
     1.7 -  |> Attributes.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (att, comment)));
     1.8 +  |> Attributes.map
     1.9 +    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
    1.10 +      (name, (att, comment)) #> snd);
    1.11  
    1.12  
    1.13  (* name space *)