avoid Theory.rep_theory;
authorwenzelm
Thu Sep 20 20:56:33 2007 +0200 (2007-09-20)
changeset 24665e5bea50b9b89
parent 24664 4195de64fdb1
child 24666 9885a86f14a8
avoid Theory.rep_theory;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Thu Sep 20 20:56:32 2007 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Sep 20 20:56:33 2007 +0200
     1.3 @@ -198,7 +198,9 @@
     1.4      fun pretty_restrict (const, name) =
     1.5        Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
     1.6  
     1.7 -    val {axioms, defs, oracles} = Theory.rep_theory thy;
     1.8 +    val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
     1.9 +    val oracles = (Theory.oracle_space thy, Theory.oracle_table thy);
    1.10 +    val defs = Theory.defs_of thy;
    1.11      val {restricts, reducts} = Defs.dest defs;
    1.12      val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
    1.13      val {constants, constraints} = Consts.dest consts;