src/Pure/sign.ML
changeset 21932 7d592dc078e3
parent 21796 481094a3dd1f
child 22086 cf6019fece63
     1.1 --- a/src/Pure/sign.ML	Fri Dec 29 17:24:41 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Dec 29 17:24:43 2006 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4    val syn_of: theory -> Syntax.syntax
     1.5    val tsig_of: theory -> Type.tsig
     1.6    val classes_of: theory -> Sorts.algebra
     1.7 -  val classes: theory -> class list
     1.8 +  val all_classes: theory -> class list
     1.9    val super_classes: theory -> class -> class list
    1.10    val defaultS: theory -> sort
    1.11    val subsort: theory -> sort * sort -> bool
    1.12 @@ -267,7 +267,8 @@
    1.13  
    1.14  val tsig_of = #tsig o rep_sg;
    1.15  val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
    1.16 -val classes = Sorts.classes o classes_of;
    1.17 +val all_classes = Sorts.all_classes o classes_of;
    1.18 +val minimal_classes = Sorts.minimal_classes o classes_of;
    1.19  val super_classes = Sorts.super_classes o classes_of;
    1.20  val defaultS = Type.defaultS o tsig_of;
    1.21  val subsort = Type.subsort o tsig_of;