--- a/src/Pure/axclass.ML Thu Mar 25 21:14:15 2010 +0100
+++ b/src/Pure/axclass.ML Thu Mar 25 21:27:04 2010 +0100
@@ -187,7 +187,7 @@
Sign.super_classes thy c
|> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
- val completions = map (fn c1 => (Sorts.weaken algebra
+ val completions = map (fn c1 => (Sorts.classrel_derivation algebra
(fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
|> Thm.close_derivation, c1)) super_class_completions;
val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))