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