src/Pure/drule.ML
changeset 400 3c2c40c87112
parent 385 921f87897a76
child 561 95225e63ef02
     1.1 --- a/src/Pure/drule.ML	Thu May 26 16:43:24 1994 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu May 26 16:43:48 1994 +0200
     1.3 @@ -85,6 +85,8 @@
     1.4  structure Sign = Thm.Sign;
     1.5  structure Type = Sign.Type;
     1.6  structure Pretty = Sign.Syntax.Pretty
     1.7 +structure Symtab = Sign.Symtab;
     1.8 +
     1.9  local open Thm
    1.10  in
    1.11  
    1.12 @@ -188,8 +190,8 @@
    1.13  
    1.14  fun print_axioms thy =
    1.15    let
    1.16 -    val {sign, ext_axtab, ...} = rep_theory thy;
    1.17 -    val axioms = Symtab.dest ext_axtab;
    1.18 +    val {sign, new_axioms, ...} = rep_theory thy;
    1.19 +    val axioms = Symtab.dest new_axioms;
    1.20  
    1.21      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
    1.22        Pretty.quote (Sign.pretty_term sign t)];