src/Pure/axclass.ML
changeset 27554 2deaa546ba0d
parent 27547 13199740ced6
child 27683 add9a605d562
     1.1 --- a/src/Pure/axclass.ML	Fri Jul 11 16:56:20 2008 +0200
     1.2 +++ b/src/Pure/axclass.ML	Fri Jul 11 23:17:23 2008 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4        |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
     1.5            andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t))
     1.6      val tags = Thm.get_tags th;
     1.7 -    val completions = map (fn c1 => (Sorts.weaken ((#classes o Sorts.rep_algebra) algebra)
     1.8 +    val completions = map (fn c1 => (Sorts.weaken algebra
     1.9        (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
    1.10          |> Thm.map_tags (K tags) |> Thm.close_derivation, c1)) super_class_completions;
    1.11      val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), th1)))