src/Pure/sign.ML
changeset 21932 7d592dc078e3
parent 21796 481094a3dd1f
child 22086 cf6019fece63
--- a/src/Pure/sign.ML	Fri Dec 29 17:24:41 2006 +0100
+++ b/src/Pure/sign.ML	Fri Dec 29 17:24:43 2006 +0100
@@ -93,7 +93,7 @@
   val syn_of: theory -> Syntax.syntax
   val tsig_of: theory -> Type.tsig
   val classes_of: theory -> Sorts.algebra
-  val classes: theory -> class list
+  val all_classes: theory -> class list
   val super_classes: theory -> class -> class list
   val defaultS: theory -> sort
   val subsort: theory -> sort * sort -> bool
@@ -267,7 +267,8 @@
 
 val tsig_of = #tsig o rep_sg;
 val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
-val classes = Sorts.classes o classes_of;
+val all_classes = Sorts.all_classes o classes_of;
+val minimal_classes = Sorts.minimal_classes o classes_of;
 val super_classes = Sorts.super_classes o classes_of;
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;