--- 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)];