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; |