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 ****)