diff -r 7b60621e2bad -r df8f91c0e57c src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Dec 09 13:39:52 1994 +0100
+++ b/src/Pure/drule.ML	Fri Dec 09 16:42:09 1994 +0100
@@ -110,7 +110,8 @@
 fun ancestry_of thy =
   thy :: flat (map ancestry_of (parents_of thy));
 
-val all_axioms_of = flat o map axioms_of o ancestry_of;
+val all_axioms_of = 
+  flat o map (Symtab.dest o #new_axioms o rep_theory) o ancestry_of;
 
 
 (* clash_types, clash_consts *)