src/Pure/sign.ML
changeset 35680 897740382442
parent 35669 a91c7ed801b8
child 35800 76b2a53a199d
     1.1 --- a/src/Pure/sign.ML	Tue Mar 09 23:27:35 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Mar 09 23:29:04 2010 +0100
     1.3 @@ -47,6 +47,9 @@
     1.4    val class_space: theory -> Name_Space.T
     1.5    val type_space: theory -> Name_Space.T
     1.6    val const_space: theory -> Name_Space.T
     1.7 +  val class_alias: binding -> class -> theory -> theory
     1.8 +  val type_alias: binding -> string -> theory -> theory
     1.9 +  val const_alias: binding -> string -> theory -> theory
    1.10    val intern_class: theory -> xstring -> string
    1.11    val extern_class: theory -> string -> xstring
    1.12    val intern_type: theory -> xstring -> string
    1.13 @@ -233,6 +236,10 @@
    1.14  val type_space = Type.type_space o tsig_of;
    1.15  val const_space = Consts.space_of o consts_of;
    1.16  
    1.17 +fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
    1.18 +fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
    1.19 +fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
    1.20 +
    1.21  val intern_class = Name_Space.intern o class_space;
    1.22  val extern_class = Name_Space.extern o class_space;
    1.23  val intern_type = Name_Space.intern o type_space;