# HG changeset patch
# User wenzelm
# Date 1125496003 -7200
# Node ID 6f0f8b6cd3f35ad2133700ec4ef76246f369704d
# Parent  29b2563f5c11154ad1afe6ceb9743c04d8449ca2
tuned classes_arities_of;

diff -r 29b2563f5c11 -r 6f0f8b6cd3f3 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;