export arities_of instead of classes_arities_of;
authorwenzelm
Sat, 18 Mar 2006 20:10:48 +0100
changeset 19289 1fc9a2e3a1b7
parent 19288 85b684d3fdbd
child 19290 033c3ade1e84
export arities_of instead of classes_arities_of;
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;