added all_super_classes
authorhaftmann
Thu, 17 Aug 2006 09:24:49 +0200
changeset 20391 d079804d3b82
parent 20390 c80247278cb6
child 20392 88cab786d024
added all_super_classes
src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Thu Aug 17 09:24:48 2006 +0200
+++ b/src/Pure/sorts.ML	Thu Aug 17 09:24:49 2006 +0200
@@ -30,6 +30,7 @@
     arities: (class * (class * sort list)) list Symtab.table}
   val classes: algebra -> class list
   val super_classes: algebra -> class -> class list
+  val all_super_classes: algebra -> class -> class list
   val class_less: algebra -> class * class -> bool
   val class_le: algebra -> class * class -> bool
   val sort_eq: algebra -> sort * sort -> bool
@@ -122,6 +123,7 @@
 
 val classes = Graph.keys o classes_of;
 val super_classes = Graph.imm_succs o classes_of;
+fun all_super_classes algebra class = Graph.all_succs (classes_of algebra) [class];
 
 
 (* class relations *)