diff -r 86cc2b98f9e0 -r 3c2c40c87112 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu May 26 16:43:24 1994 +0200
+++ b/src/Pure/drule.ML	Thu May 26 16:43:48 1994 +0200
@@ -85,6 +85,8 @@
 structure Sign = Thm.Sign;
 structure Type = Sign.Type;
 structure Pretty = Sign.Syntax.Pretty
+structure Symtab = Sign.Symtab;
+
 local open Thm
 in
 
@@ -188,8 +190,8 @@
 
 fun print_axioms thy =
   let
-    val {sign, ext_axtab, ...} = rep_theory thy;
-    val axioms = Symtab.dest ext_axtab;
+    val {sign, new_axioms, ...} = rep_theory thy;
+    val axioms = Symtab.dest new_axioms;
 
     fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
       Pretty.quote (Sign.pretty_term sign t)];