added Local_Theory.alias operations (independent of target);
authorwenzelm
Sat Mar 13 14:40:36 2010 +0100 (2010-03-13 ago)
changeset 3573898fd035c3fe3
parent 35737 19eefc0655b6
child 35739 35a3b3721ffb
added Local_Theory.alias operations (independent of target);
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Thu Mar 11 23:47:16 2010 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Mar 13 14:40:36 2010 +0100
     1.3 @@ -44,6 +44,9 @@
     1.4    val declaration: bool -> declaration -> local_theory -> local_theory
     1.5    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
     1.6    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     1.7 +  val class_alias: binding -> class -> local_theory -> local_theory
     1.8 +  val type_alias: binding -> string -> local_theory -> local_theory
     1.9 +  val const_alias: binding -> string -> local_theory -> local_theory
    1.10    val init: serial option -> string -> operations -> Proof.context -> local_theory
    1.11    val restore: local_theory -> local_theory
    1.12    val reinit: local_theory -> local_theory
    1.13 @@ -199,6 +202,9 @@
    1.14  val notes = notes_kind "";
    1.15  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
    1.16  
    1.17 +
    1.18 +(* notation *)
    1.19 +
    1.20  fun type_notation add mode raw_args lthy =
    1.21    let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
    1.22    in type_syntax false (ProofContext.target_type_notation add mode args) lthy end;
    1.23 @@ -208,6 +214,19 @@
    1.24    in term_syntax false (ProofContext.target_notation add mode args) lthy end;
    1.25  
    1.26  
    1.27 +(* name space aliases *)
    1.28 +
    1.29 +fun alias syntax_declaration global_alias local_alias b name =
    1.30 +  syntax_declaration false (fn phi =>
    1.31 +    let val b' = Morphism.binding phi b
    1.32 +    in Context.mapping (global_alias b' name) (local_alias b' name) end)
    1.33 +  #> local_alias b name;
    1.34 +
    1.35 +val class_alias = alias type_syntax Sign.class_alias ProofContext.class_alias;
    1.36 +val type_alias = alias type_syntax Sign.type_alias ProofContext.type_alias;
    1.37 +val const_alias = alias term_syntax Sign.const_alias ProofContext.const_alias;
    1.38 +
    1.39 +
    1.40  (* init *)
    1.41  
    1.42  fun init group theory_prefix operations target =