# HG changeset patch
# User wenzelm
# Date 1190314593 -7200
# Node ID e5bea50b9b89476cbc77a992d8b8c3e1d73a0500
# Parent  4195de64fdb1c8f9e5a265b8953fb2a5247f7e09
avoid Theory.rep_theory;

diff -r 4195de64fdb1 -r e5bea50b9b89 src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Sep 20 20:56:32 2007 +0200
+++ b/src/Pure/display.ML	Thu Sep 20 20:56:33 2007 +0200
@@ -198,7 +198,9 @@
     fun pretty_restrict (const, name) =
       Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
-    val {axioms, defs, oracles} = Theory.rep_theory thy;
+    val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
+    val oracles = (Theory.oracle_space thy, Theory.oracle_table thy);
+    val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
     val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
     val {constants, constraints} = Consts.dest consts;