src/Pure/Isar/local_theory.ML

   val pretty: local_theory -> Pretty.T list
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val generic_alias:
-    (('a Name_Space.table -> 'a Name_Space.table) -> Context.generic -> Context.generic) ->
-    binding -> string -> local_theory -> local_theory
   val class_alias: binding -> class -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: Name_Space.naming -> operations -> Proof.context -> local_theory
   val exit: local_theory -> Proof.context

   end;
 
 
 (* name space aliases *)
 
-fun generic_alias app b name =
-  declaration {syntax = false, pervasive = false} (fn phi => fn context =>
-    let
-      val naming = Name_Space.naming_of context;
-      val b' = Morphism.binding phi b;
-    in app (Name_Space.alias_table naming b' name) context end);
-
 fun syntax_alias global_alias local_alias b name =
   declaration {syntax = true, pervasive = false} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);