# HG changeset patch
# User wenzelm
# Date 1526216731 -7200
# Node ID 738071699826eec2c743cb3ec7398f2c0bb0dbe1
# Parent  b168f30e541f94226c26cea2be6d0514abf79b32
tuned;

diff -r b168f30e541f -r 738071699826 src/Pure/theory.ML
--- 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;