src/Pure/display.ML

     fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
     val prt_const' = Defs.pretty_const ctxt;
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
-          (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 ::
-            Pretty.commas (map prt_cls cs));
+          (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
 
     fun pretty_default S = Pretty.block
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
     val tfrees = map (fn v => TFree (v, []));

     val consts = Sign.consts_of thy;
     val {constants, constraints} = Consts.dest consts;
     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 (fn ((c, _), cs) => (c, sort class_ord cs)) (Graph.dest classes)));
+        Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)));
     val tdecls = Name_Space.dest_table ctxt types;
     val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);
 
     fun prune_const c = not verbose andalso Consts.is_concealed consts c;
     val cnsts = Name_Space.extern_table ctxt (#1 constants,