added of_sort;
authorwenzelm
Wed Jan 14 10:24:57 1998 +0100 (1998-01-14)
changeset 45687be03035c553
parent 4567 b0b963a01a0c
child 4569 4fd775d5456f
added of_sort;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Tue Jan 13 18:03:37 1998 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Jan 14 10:24:57 1998 +0100
     1.3 @@ -43,6 +43,7 @@
     1.4    val nodup_Vars: term -> unit
     1.5    val norm_sort: sg -> sort -> sort
     1.6    val nonempty_sort: sg -> sort list -> sort -> bool
     1.7 +  val of_sort: sg -> typ * sort -> bool
     1.8    val long_names: bool ref
     1.9    val classK: string
    1.10    val typeK: string
    1.11 @@ -178,11 +179,6 @@
    1.12  val tsig_of = #tsig o rep_sg;
    1.13  
    1.14  fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c);
    1.15 -val classes = #classes o Type.rep_tsig o tsig_of;
    1.16 -
    1.17 -val subsort = Type.subsort o tsig_of;
    1.18 -val norm_sort = Type.norm_sort o tsig_of;
    1.19 -val nonempty_sort = Type.nonempty_sort o tsig_of;
    1.20  
    1.21  
    1.22  (* id and self *)
    1.23 @@ -244,6 +240,18 @@
    1.24    | is_draft _ = false;
    1.25  
    1.26  
    1.27 +(* classes and sorts *)
    1.28 +
    1.29 +val classes = #classes o Type.rep_tsig o tsig_of;
    1.30 +
    1.31 +val subsort = Type.subsort o tsig_of;
    1.32 +val norm_sort = Type.norm_sort o tsig_of;
    1.33 +val nonempty_sort = Type.nonempty_sort o tsig_of;
    1.34 +
    1.35 +fun of_sort (Sg (_, {tsig, ...})) =
    1.36 +  Sorts.of_sort (#classrel (Type.rep_tsig tsig)) (#arities (Type.rep_tsig tsig));
    1.37 +
    1.38 +
    1.39  
    1.40  (** signature data **)
    1.41