| changeset 19482 | 9f11af8f7ef9 |
| parent 19428 | 43bfe55759b0 |
| child 19570 | f199cb2295fd |
--- a/src/Pure/theory.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/theory.ML Thu Apr 27 15:06:35 2006 +0200 @@ -144,7 +144,7 @@ val oracle_space = #1 o #oracles o rep_theory; val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; -fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy)); +fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy); val defs_of = #defs o rep_theory;