# HG changeset patch
# User wenzelm
# Date 1167409483 -3600
# Node ID 7d592dc078e37ace7d5344e432856eb8e5d1b8f8
# Parent  314f9e2a442c895d8c6639545b6d230a0e39082e
replaced classes by all_classes (topologically sorted);
added minimal_classes;

diff -r 314f9e2a442c -r 7d592dc078e3 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;