src/Pure/consts.ML
changeset 35680 897740382442
parent 35554 1e05ea0a5cd7
child 37146 f652333bbf8e
     1.1 --- a/src/Pure/consts.ML	Tue Mar 09 23:27:35 2010 +0100
     1.2 +++ b/src/Pure/consts.ML	Tue Mar 09 23:29:04 2010 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4    val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
     1.5    val the_constraint: T -> string -> typ                       (*exception TYPE*)
     1.6    val space_of: T -> Name_Space.T
     1.7 +  val alias: Name_Space.naming -> binding -> string -> T -> T
     1.8    val is_concealed: T -> string -> bool
     1.9    val intern: T -> xstring -> string
    1.10    val extern: T -> string -> xstring
    1.11 @@ -122,6 +123,9 @@
    1.12  
    1.13  fun space_of (Consts {decls = (space, _), ...}) = space;
    1.14  
    1.15 +fun alias naming binding name = map_consts (fn ((space, decls), constraints, rev_abbrevs) =>
    1.16 +  ((Name_Space.alias naming binding name space, decls), constraints, rev_abbrevs));
    1.17 +
    1.18  val is_concealed = Name_Space.is_concealed o space_of;
    1.19  
    1.20  val intern = Name_Space.intern o space_of;