--- a/src/Pure/sign.ML Tue Mar 09 23:27:35 2010 +0100
+++ b/src/Pure/sign.ML Tue Mar 09 23:29:04 2010 +0100
@@ -47,6 +47,9 @@
val class_space: theory -> Name_Space.T
val type_space: theory -> Name_Space.T
val const_space: theory -> Name_Space.T
+ val class_alias: binding -> class -> theory -> theory
+ val type_alias: binding -> string -> theory -> theory
+ val const_alias: binding -> string -> theory -> theory
val intern_class: theory -> xstring -> string
val extern_class: theory -> string -> xstring
val intern_type: theory -> xstring -> string
@@ -233,6 +236,10 @@
val type_space = Type.type_space o tsig_of;
val const_space = Consts.space_of o consts_of;
+fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
+fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
+fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
+
val intern_class = Name_Space.intern o class_space;
val extern_class = Name_Space.extern o class_space;
val intern_type = Name_Space.intern o type_space;