# HG changeset patch
# User wenzelm
# Date 884769897 -3600
# Node ID 7be03035c5530cd1a3bd66ff03b9916d480eb9f3
# Parent  b0b963a01a0cd17f8d918c2fc01ea418599fb2b3
added of_sort;

diff -r b0b963a01a0c -r 7be03035c553 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Jan 13 18:03:37 1998 +0100
+++ b/src/Pure/sign.ML	Wed Jan 14 10:24:57 1998 +0100
@@ -43,6 +43,7 @@
   val nodup_Vars: term -> unit
   val norm_sort: sg -> sort -> sort
   val nonempty_sort: sg -> sort list -> sort -> bool
+  val of_sort: sg -> typ * sort -> bool
   val long_names: bool ref
   val classK: string
   val typeK: string
@@ -178,11 +179,6 @@
 val tsig_of = #tsig o rep_sg;
 
 fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c);
-val classes = #classes o Type.rep_tsig o tsig_of;
-
-val subsort = Type.subsort o tsig_of;
-val norm_sort = Type.norm_sort o tsig_of;
-val nonempty_sort = Type.nonempty_sort o tsig_of;
 
 
 (* id and self *)
@@ -244,6 +240,18 @@
   | is_draft _ = false;
 
 
+(* classes and sorts *)
+
+val classes = #classes o Type.rep_tsig o tsig_of;
+
+val subsort = Type.subsort o tsig_of;
+val norm_sort = Type.norm_sort o tsig_of;
+val nonempty_sort = Type.nonempty_sort o tsig_of;
+
+fun of_sort (Sg (_, {tsig, ...})) =
+  Sorts.of_sort (#classrel (Type.rep_tsig tsig)) (#arities (Type.rep_tsig tsig));
+
+
 
 (** signature data **)