src/Pure/sign.ML
changeset 19642 ea7162f84677
parent 19513 77ff7cd602d7
child 19658 0cff73279f34
     1.1 --- a/src/Pure/sign.ML	Tue May 16 13:01:23 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue May 16 13:01:24 2006 +0200
     1.3 @@ -94,8 +94,7 @@
     1.4    val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
     1.5    val syn_of: theory -> Syntax.syntax
     1.6    val tsig_of: theory -> Type.tsig
     1.7 -  val classes_of: theory -> Sorts.classes
     1.8 -  val arities_of: theory -> Sorts.arities
     1.9 +  val classes_of: theory -> Sorts.algebra
    1.10    val classes: theory -> class list
    1.11    val super_classes: theory -> class -> class list
    1.12    val defaultS: theory -> sort
    1.13 @@ -267,10 +266,9 @@
    1.14  (* type signature *)
    1.15  
    1.16  val tsig_of = #tsig o rep_sg;
    1.17 -val classes_of = snd o #classes o Type.rep_tsig o tsig_of;
    1.18 -val arities_of = #arities o Type.rep_tsig o tsig_of;
    1.19 -val classes = Type.classes o tsig_of;
    1.20 -val super_classes = Graph.imm_succs o classes_of;
    1.21 +val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
    1.22 +val classes = Sorts.classes o classes_of;
    1.23 +val super_classes = Sorts.super_classes o classes_of;
    1.24  val defaultS = Type.defaultS o tsig_of;
    1.25  val subsort = Type.subsort o tsig_of;
    1.26  val of_sort = Type.of_sort o tsig_of;