replaced classes by all_classes (topologically sorted);
authorwenzelm
Fri, 29 Dec 2006 17:24:43 +0100
changeset 21932 7d592dc078e3
parent 21931 314f9e2a442c
child 21933 819ef284720b
replaced classes by all_classes (topologically sorted); added minimal_classes;
src/Pure/sign.ML
--- 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;