diff -r f1de44e61ec1 -r ea7162f84677 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue May 16 13:01:23 2006 +0200
+++ b/src/Pure/display.ML	Tue May 16 13:01:24 2006 +0200
@@ -212,9 +212,11 @@
     val {axioms, defs = _, oracles} = Theory.rep_theory thy;
     val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
     val {constants, constraints} = Consts.dest consts;
-    val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
+    val {classes = (class_space, class_algebra),
+      default, types, log_types = _, witness} = Type.rep_tsig tsig;
+    val {classes, arities} = Sorts.rep_algebra class_algebra;
 
-    val clsses = NameSpace.dest_table (apsnd (Symtab.make o Graph.dest) classes);
+    val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
     val tdecls = NameSpace.dest_table types;
     val arties = NameSpace.dest_table (Sign.type_space thy, arities);
     val cnsts = NameSpace.extern_table constants;