# HG changeset patch
# User wenzelm
# Date 1146495909 -7200
# Node ID cfdab6a91332d0ee3a7a9c5f0cf3cea331b47cab
# Parent  873dad2d8a6d57fe00624d38c5d83997b9725ebe
adapted arities;

diff -r 873dad2d8a6d -r cfdab6a91332 src/HOL/Tools/res_clause.ML
--- 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 ****)
diff -r 873dad2d8a6d -r cfdab6a91332 src/Pure/display.ML
--- 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);