added super_classes (from sorts.ML);
authorwenzelm
Tue Apr 11 16:00:03 2006 +0200 (2006-04-11)
changeset 194077c7a2e337504
parent 19406 410b9d9bf9a1
child 19408 9a52d5b7fc27
added super_classes (from sorts.ML);
removed read/cert_classrel (see axclass.ML);
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Apr 11 16:00:02 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Apr 11 16:00:03 2006 +0200
     1.3 @@ -100,6 +100,7 @@
     1.4    val classes_of: theory -> Sorts.classes
     1.5    val arities_of: theory -> Sorts.arities
     1.6    val classes: theory -> class list
     1.7 +  val super_classes: theory -> class -> class list
     1.8    val defaultS: theory -> sort
     1.9    val subsort: theory -> sort * sort -> bool
    1.10    val of_sort: theory -> typ * sort -> bool
    1.11 @@ -165,8 +166,6 @@
    1.12    val read_class: theory -> xstring -> class
    1.13    val read_sort': Syntax.syntax -> Context.generic -> string -> sort
    1.14    val read_sort: theory -> string -> sort
    1.15 -  val read_classrel: theory -> xstring * xstring -> class * class
    1.16 -  val cert_classrel: theory -> class * class -> class * class
    1.17    val read_arity: theory -> xstring * string list * string -> arity
    1.18    val cert_arity: theory -> arity -> arity
    1.19    val read_typ': Syntax.syntax -> Context.generic ->
    1.20 @@ -271,6 +270,7 @@
    1.21  val classes_of = snd o #classes o Type.rep_tsig o tsig_of;
    1.22  val arities_of = #arities o Type.rep_tsig o tsig_of;
    1.23  val classes = Type.classes o tsig_of;
    1.24 +val super_classes = Graph.imm_succs o classes_of;
    1.25  val defaultS = Type.defaultS o tsig_of;
    1.26  val subsort = Type.subsort o tsig_of;
    1.27  val of_sort = Type.of_sort o tsig_of;
    1.28 @@ -515,16 +515,6 @@
    1.29  fun read_sort thy str = read_sort' (syn_of thy) (Context.Theory thy) str;
    1.30  
    1.31  
    1.32 -(* class relations *)
    1.33 -
    1.34 -fun prep_classrel prep thy raw_rel =
    1.35 -  let val rel = Library.pairself (prep thy) raw_rel
    1.36 -  in Type.add_classrel (pp thy) [rel] (tsig_of thy); rel end;
    1.37 -
    1.38 -val read_classrel = prep_classrel read_class;
    1.39 -val cert_classrel = prep_classrel certify_class;
    1.40 -
    1.41 -
    1.42  (* type arities *)
    1.43  
    1.44  fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =