adapted arities;

--- a/src/HOL/Tools/res_clause.ML	Mon May 01 01:22:31 2006 +0200
+++ b/src/HOL/Tools/res_clause.ML	Mon May 01 17:05:09 2006 +0200
@@ -713,8 +713,9 @@
       multi_arity_clause tc_arlists 
 
 fun arity_clause_thy thy =
-  let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy))
-  in multi_arity_clause (rev (Symtab.dest arities)) end;
+  let val arities =
+    Symtab.dest (Sign.arities_of thy) |> map (apsnd (map (fn (c, (_, Ss)) => (c, Ss))));
+  in multi_arity_clause (rev arities) end;
 
 
 (**** Find occurrences of predicates in clauses ****)

--- a/src/Pure/display.ML	Mon May 01 01:22:31 2006 +0200
+++ b/src/Pure/display.ML	Mon May 01 17:05:09 2006 +0200
@@ -157,7 +157,7 @@
   let
     fun prt_cls c = Sign.pretty_sort thy [c];
     fun prt_sort S = Sign.pretty_sort thy S;
-    fun prt_arity t (c, Ss) = Sign.pretty_arity thy (t, Ss, [c]);
+    fun prt_arity t (c, (_, Ss)) = Sign.pretty_arity thy (t, Ss, [c]);
     fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
     val prt_typ_no_tvars = prt_typ o Type.freeze_type;
     fun prt_term t = Pretty.quote (Sign.pretty_term thy t);