export arities_of instead of classes_arities_of;
authorwenzelm
Sat Mar 18 20:10:48 2006 +0100 (2006-03-18)
changeset 192891fc9a2e3a1b7
parent 19288 85b684d3fdbd
child 19290 033c3ade1e84
export arities_of instead of classes_arities_of;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Sat Mar 18 18:33:49 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Mar 18 20:10:48 2006 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4    val syn_of: theory -> Syntax.syntax
     1.5    val tsig_of: theory -> Type.tsig
     1.6    val classes_of: theory -> Sorts.classes
     1.7 -  val classes_arities_of: theory -> Sorts.classes * Sorts.arities
     1.8 +  val arities_of: theory -> Sorts.arities
     1.9    val classes: theory -> class list
    1.10    val defaultS: theory -> sort
    1.11    val subsort: theory -> sort * sort -> bool
    1.12 @@ -269,7 +269,7 @@
    1.13  
    1.14  val tsig_of = #tsig o rep_sg;
    1.15  val classes_of = snd o #classes o Type.rep_tsig o tsig_of;
    1.16 -fun classes_arities_of thy = (classes_of thy, #arities (Type.rep_tsig (tsig_of thy)));
    1.17 +val arities_of = #arities o Type.rep_tsig o tsig_of;
    1.18  val classes = Type.classes o tsig_of;
    1.19  val defaultS = Type.defaultS o tsig_of;
    1.20  val subsort = Type.subsort o tsig_of;