# HG changeset patch
# User wenzelm
# Date 1142709048 -3600
# Node ID 1fc9a2e3a1b7905464e469a460f966031497ffde
# Parent  85b684d3fdbdab82ec52f541a38e84b7cb58b38b
export arities_of instead of classes_arities_of;

diff -r 85b684d3fdbd -r 1fc9a2e3a1b7 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Mar 18 18:33:49 2006 +0100
+++ b/src/Pure/sign.ML	Sat Mar 18 20:10:48 2006 +0100
@@ -98,7 +98,7 @@
   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 arities_of: theory -> Sorts.arities
   val classes: theory -> class list
   val defaultS: theory -> sort
   val subsort: theory -> sort * sort -> bool
@@ -269,7 +269,7 @@
 
 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 = (classes_of thy, #arities (Type.rep_tsig (tsig_of thy)));
+val arities_of = #arities o Type.rep_tsig o tsig_of;
 val classes = Type.classes o tsig_of;
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;