equal
deleted
inserted
replaced
108 (*results may contain duplicates!*) |
108 (*results may contain duplicates!*) |
109 |
109 |
110 fun ancestry_of thy = |
110 fun ancestry_of thy = |
111 thy :: flat (map ancestry_of (parents_of thy)); |
111 thy :: flat (map ancestry_of (parents_of thy)); |
112 |
112 |
113 val all_axioms_of = flat o map axioms_of o ancestry_of; |
113 val all_axioms_of = |
|
114 flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of; |
114 |
115 |
115 |
116 |
116 (* clash_types, clash_consts *) |
117 (* clash_types, clash_consts *) |
117 |
118 |
118 (*check if types have common instance (ignoring sorts)*) |
119 (*check if types have common instance (ignoring sorts)*) |