added Local_Theory.alias operations (independent of target);

--- a/src/Pure/Isar/local_theory.ML	Thu Mar 11 23:47:16 2010 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sat Mar 13 14:40:36 2010 +0100
@@ -44,6 +44,9 @@
   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
@@ -199,6 +202,9 @@
 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;
@@ -208,6 +214,19 @@
   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 =