src/Pure/Isar/attrib.ML

   let val att0 = att o Args.transform_values (Local_Theory.background_morphism lthy) in
     lthy
     |> Local_Theory.background_theory_result (define_global binding att0 comment)
     |-> (fn name =>
       Local_Theory.map_contexts (K transfer_attributes)
-      #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
-          let
-            val naming = Name_Space.naming_of context;
-            val binding' = Morphism.binding phi binding;
-          in Attributes.map (Name_Space.alias_table naming binding' name) context end)
+      #> Local_Theory.generic_alias Attributes.map binding name
       #> pair name)
   end;
 
 
 (* check *)