tuned classes_arities_of;
authorwenzelm
Wed, 31 Aug 2005 15:46:43 +0200
changeset 17204 6f0f8b6cd3f3
parent 17203 29b2563f5c11
child 17205 8994750ae33c
tuned classes_arities_of;
src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Aug 31 15:46:40 2005 +0200
+++ b/src/Pure/sign.ML	Wed Aug 31 15:46:43 2005 +0200
@@ -263,11 +263,8 @@
 (* 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_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 classes = Type.classes o tsig_of;
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;