1.1 --- a/src/Pure/sorts.ML	Mon Dec 01 12:16:59 2008 +0100
     1.2 +++ b/src/Pure/sorts.ML	Mon Dec 01 12:17:00 2008 +0100
     1.3 @@ -47,6 +47,8 @@
     1.4    val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
     1.5    val empty_algebra: algebra
     1.6    val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
     1.7 +  val classrels_of: algebra -> (class * class list) list
     1.8 +  val instances_of: algebra -> (string * class) list
     1.9    val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
    1.10      -> algebra -> (sort -> sort) * algebra
    1.11    type class_error
    1.12 @@ -299,7 +301,13 @@
    1.13    in make_algebra (classes', arities') end;
    1.14  
    1.15  
    1.16 -(* subalgebra *)
    1.17 +(* algebra projections *)
    1.18 +
    1.19 +fun classrels_of (Algebra {classes, ...}) =
    1.20 +  map (fn [c] => (c, Graph.imm_succs classes c)) (rev (Graph.strong_conn classes));
    1.21 +
    1.22 +fun instances_of (Algebra {arities, ...}) =
    1.23 +  Symtab.fold (fn (a, cs) => append (map (pair a o fst) cs)) arities [];
    1.24  
    1.25  fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
    1.26    let