src/Pure/sorts.ML
changeset 20391 d079804d3b82
parent 19977 ac1b062c81ac
child 20454 7e948db7e42d
     1.1 --- a/src/Pure/sorts.ML	Thu Aug 17 09:24:48 2006 +0200
     1.2 +++ b/src/Pure/sorts.ML	Thu Aug 17 09:24:49 2006 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4      arities: (class * (class * sort list)) list Symtab.table}
     1.5    val classes: algebra -> class list
     1.6    val super_classes: algebra -> class -> class list
     1.7 +  val all_super_classes: algebra -> class -> class list
     1.8    val class_less: algebra -> class * class -> bool
     1.9    val class_le: algebra -> class * class -> bool
    1.10    val sort_eq: algebra -> sort * sort -> bool
    1.11 @@ -122,6 +123,7 @@
    1.12  
    1.13  val classes = Graph.keys o classes_of;
    1.14  val super_classes = Graph.imm_succs o classes_of;
    1.15 +fun all_super_classes algebra class = Graph.all_succs (classes_of algebra) [class];
    1.16  
    1.17  
    1.18  (* class relations *)