# HG changeset patch
# User haftmann
# Date 1123578044 -7200
# Node ID 78159411623f44dc30a26c274235cdbe4e6a990a
# Parent  6dbd7c63a5a653defafcc2d894a627e9ee0b0433
added selectors 'classes_of' and 'classes_arities_of'

diff -r 6dbd7c63a5a6 -r 78159411623f 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;