# HG changeset patch
# User wenzelm
# Date 1215811043 -7200
# Node ID 2deaa546ba0d876c3fcf87015144f8e2267f6c81
# Parent  d315a513a150faf75298a90e03fb0303bd246608
Sorts.weaken: abstract argument;

diff -r d315a513a150 -r 2deaa546ba0d src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Jul 11 16:56:20 2008 +0200
+++ b/src/Pure/axclass.ML	Fri Jul 11 23:17:23 2008 +0200
@@ -194,7 +194,7 @@
       |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
           andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t))
     val tags = Thm.get_tags th;
-    val completions = map (fn c1 => (Sorts.weaken ((#classes o Sorts.rep_algebra) algebra)
+    val completions = map (fn c1 => (Sorts.weaken algebra
       (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
         |> Thm.map_tags (K tags) |> Thm.close_derivation, c1)) super_class_completions;
     val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), th1)))