src/Pure/sign.ML
changeset 66245 da3b0e848182
parent 61262 7bd1eb4b056e
child 70364 b2bedb022a75
     1.1 --- a/src/Pure/sign.ML	Sat Jul 01 16:39:56 2017 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Jul 03 09:12:13 2017 +0200
     1.3 @@ -53,7 +53,6 @@
     1.4    val intern_class: theory -> xstring -> string
     1.5    val intern_type: theory -> xstring -> string
     1.6    val intern_const: theory -> xstring -> string
     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 arity_number: theory -> string -> int
    1.11 @@ -246,7 +245,6 @@
    1.12  val intern_type = Name_Space.intern o type_space;
    1.13  val intern_const = Name_Space.intern o const_space;
    1.14  
    1.15 -fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
    1.16  fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
    1.17  fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
    1.18