tuned message;
authorwenzelm
Mon, 25 Mar 2013 11:05:07 +0100
changeset 51509 22fd3605c7a2
parent 51508 48a1e09120d4
child 51510 b4f7e6734acc
tuned message;
src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Mar 25 10:45:47 2013 +0100
+++ b/src/Pure/display.ML	Mon Mar 25 11:05:07 2013 +0100
@@ -167,11 +167,13 @@
     val extern_const = Name_Space.extern ctxt (#1 constants);
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val (class_space, class_algebra) = classes;
+    val class_ord = string_ord o pairself (Name_Space.extern ctxt class_space);
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
     val clsses =
-      Name_Space.dest_table ctxt (class_space, Symtab.make (map (apfst fst) (Graph.dest classes)));
+      Name_Space.dest_table ctxt (class_space,
+        Symtab.make (map (fn ((c, _), cs) => (c, sort class_ord cs)) (Graph.dest classes)));
     val tdecls = Name_Space.dest_table ctxt types;
     val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);