# HG changeset patch # User wenzelm # Date 1117533212 -7200 # Node ID 1e2bed9c06f794f76adacf8566b049602f31da33 # Parent fc51e61d45fb4de32ed22ce6a2d4a432073b4052 renamed cond_extern to extern; Sign.declare_name replaces NameSpace.extend; diff -r fc51e61d45fb -r 1e2bed9c06f7 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue May 31 11:53:31 2005 +0200 +++ b/src/Pure/Isar/attrib.ML Tue May 31 11:53:32 2005 +0200 @@ -75,7 +75,7 @@ fun prt_attr (name, ((_, comment), _)) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; in - [Pretty.big_list "attributes:" (map prt_attr (NameSpace.cond_extern_table space attrs))] + [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table space attrs))] |> Pretty.chunks |> Pretty.writeln end; end; @@ -140,12 +140,12 @@ fun add_attributes raw_attrs thy = let - val full = Sign.full_name (Theory.sign_of thy); - val new_attrs = - map (fn (name, (f, g), comment) => (full name, (((f, g), comment), stamp ()))) raw_attrs; + val sg = Theory.sign_of thy; + val new_attrs = raw_attrs |> map (fn (name, (f, g), comment) => + (Sign.full_name sg name, (((f, g), comment), stamp ()))); val {space, attrs} = AttributesData.get thy; - val space' = NameSpace.extend (space, map fst new_attrs); + val space' = fold (Sign.declare_name sg) (map fst new_attrs) space; val attrs' = Symtab.extend (attrs, new_attrs) handle Symtab.DUPS dups => error ("Duplicate declaration of attributes(s) " ^ commas_quote dups); in thy |> AttributesData.put {space = space', attrs = attrs'} end;