stripped classrels_of, instances_of
authorhaftmann
Mon Feb 23 10:07:57 2009 +0100 (2009-02-23)
changeset 30065c9a1e0f7621b
parent 30064 3cd19b113854
child 30071 be46f437ace2
child 30076 f3043dafef5f
stripped classrels_of, instances_of
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Mon Feb 23 08:19:25 2009 +0100
     1.2 +++ b/src/Pure/sorts.ML	Mon Feb 23 10:07:57 2009 +0100
     1.3 @@ -46,8 +46,6 @@
     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 option)
    1.10      -> algebra -> (sort -> sort) * algebra
    1.11    type class_error
    1.12 @@ -302,22 +300,6 @@
    1.13  
    1.14  (* algebra projections *)
    1.15  
    1.16 -val sorted_classes = rev o flat o Graph.strong_conn o classes_of;
    1.17 -
    1.18 -fun classrels_of algebra = 
    1.19 -  map (fn c => (c, Graph.imm_succs (classes_of algebra) c)) (sorted_classes algebra);
    1.20 -
    1.21 -fun instances_of algebra =
    1.22 -  let
    1.23 -    val arities = arities_of algebra;
    1.24 -    val all_classes = sorted_classes algebra;
    1.25 -    fun sort_classes cs = filter (member (op = o apsnd fst) cs)
    1.26 -      all_classes;
    1.27 -  in
    1.28 -    Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
    1.29 -      arities []
    1.30 -  end;
    1.31 -
    1.32  fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
    1.33    let
    1.34      val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;