# 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 **)