src/Pure/axclass.ML
changeset 27554 2deaa546ba0d
parent 27547 13199740ced6
child 27683 add9a605d562
equal deleted inserted replaced
27553:d315a513a150 27554:2deaa546ba0d
   192     val algebra = Sign.classes_of thy;
   192     val algebra = Sign.classes_of thy;
   193     val super_class_completions = Sign.super_classes thy c
   193     val super_class_completions = Sign.super_classes thy c
   194       |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
   194       |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
   195           andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t))
   195           andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t))
   196     val tags = Thm.get_tags th;
   196     val tags = Thm.get_tags th;
   197     val completions = map (fn c1 => (Sorts.weaken ((#classes o Sorts.rep_algebra) algebra)
   197     val completions = map (fn c1 => (Sorts.weaken algebra
   198       (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
   198       (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
   199         |> Thm.map_tags (K tags) |> Thm.close_derivation, c1)) super_class_completions;
   199         |> Thm.map_tags (K tags) |> Thm.close_derivation, c1)) super_class_completions;
   200     val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), th1)))
   200     val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), th1)))
   201       completions arities;
   201       completions arities;
   202   in (completions, arities') end;
   202   in (completions, arities') end;