src/HOL/Tools/res_clause.ML

       (*Reversal ensures that older entries always get the same axiom name*)
       arity_clause 0 (tcons, rev ars)  @  
       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 ****)
 
 (*FIXME: multiple-arity checking doesn't work, as update_new is the wrong