# HG changeset patch
# User haftmann
# Date 1155799489 -7200
# Node ID d079804d3b82d61b6d539859e594523c435ceb13
# Parent  c80247278cb6fdb0fa84b1670bc81d7c7b0b0c9a
added all_super_classes

diff -r c80247278cb6 -r d079804d3b82 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 *)