diff -r 48a1e09120d4 -r 22fd3605c7a2 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);