changeset 68164 | 738071699826 |
parent 67384 | e32b0eb63666 |
child 68482 | cb84beb84ca9 |
--- a/src/Pure/theory.ML Sun May 13 15:05:21 2018 +0200 +++ b/src/Pure/theory.ML Sun May 13 15:05:31 2018 +0200 @@ -157,7 +157,7 @@ val axiom_table = #axioms o rep_theory; val axiom_space = Name_Space.space_of_table o axiom_table; -fun axioms_of thy = rev (Name_Space.fold_table cons (axiom_table thy) []); +val axioms_of = Name_Space.dest_table o axiom_table; fun all_axioms_of thy = maps axioms_of (nodes_of thy); val defs_of = #defs o rep_theory;