1.1 --- a/src/Pure/Isar/attrib.ML	Fri Dec 05 11:42:27 2008 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Dec 05 18:42:37 2008 +0100
     1.3 @@ -146,8 +146,8 @@
     1.4  fun add_attributes raw_attrs thy =
     1.5    let
     1.6      val new_attrs =
     1.7 -      raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
     1.8 -    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
     1.9 +      raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
    1.10 +    fun add attrs = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_attrs attrs
    1.11        handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
    1.12    in Attributes.map add thy end;
    1.13