added selectors 'classes_of' and 'classes_arities_of'
authorhaftmann
Tue, 09 Aug 2005 11:00:44 +0200
changeset 17039 78159411623f
parent 17038 6dbd7c63a5a6
child 17040 6682c93b7d9f
added selectors 'classes_of' and 'classes_arities_of'
src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Aug 09 10:23:14 2005 +0200
+++ b/src/Pure/sign.ML	Tue Aug 09 11:00:44 2005 +0200
@@ -86,6 +86,8 @@
   val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
   val syn_of: theory -> Syntax.syntax
   val tsig_of: theory -> Type.tsig
+  val classes_of: theory -> Sorts.classes
+  val classes_arities_of: theory -> Sorts.classes * Sorts.arities
   val classes: theory -> class list
   val defaultS: theory -> sort
   val subsort: theory -> sort * sort -> bool
@@ -255,6 +257,11 @@
 (* type signature *)
 
 val tsig_of = #tsig o rep_sg;
+val classes_of = snd o #classes o Type.rep_tsig o tsig_of
+fun classes_arities_of thy =
+  let
+    val tsig = (Type.rep_tsig o tsig_of) thy
+  in (snd (#classes tsig), #arities tsig) end
 val classes = Type.classes o tsig_of;
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;