src/Pure/Isar/local_theory.ML

   val type_syntax: bool -> declaration -> local_theory -> local_theory
   val term_syntax: bool -> declaration -> local_theory -> local_theory
   val declaration: bool -> declaration -> 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 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: serial option -> string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
   val reinit: local_theory -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory

 val declaration = checkpoint ooo operation2 #declaration;
 
 val notes = notes_kind "";
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
 
+
+(* notation *)
+
 fun type_notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
   in type_syntax false (ProofContext.target_type_notation add mode args) lthy end;
 
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   in term_syntax false (ProofContext.target_notation add mode args) lthy end;
+
+
+(* name space aliases *)
+
+fun alias syntax_declaration global_alias local_alias b name =
+  syntax_declaration false (fn phi =>
+    let val b' = Morphism.binding phi b
+    in Context.mapping (global_alias b' name) (local_alias b' name) end)
+  #> local_alias b name;
+
+val class_alias = alias type_syntax Sign.class_alias ProofContext.class_alias;
+val type_alias = alias type_syntax Sign.type_alias ProofContext.type_alias;
+val const_alias = alias term_syntax Sign.const_alias ProofContext.const_alias;
 
 
 (* init *)
 
 fun init group theory_prefix operations target =