src/Pure/display.ML

--- a/src/Pure/display.ML	Tue Sep 22 08:38:25 2015 +0200
+++ b/src/Pure/display.ML	Tue Sep 22 14:32:23 2015 +0200
@@ -104,7 +104,8 @@
     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
     val prt_term_no_vars = prt_term o Logic.unvarify_global;
     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;
+    val prt_node = Defs.pretty_node ctxt;
+    fun sort_node_wrt f = sort (Defs.fast_node_ord o apply2 f)
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
@@ -134,26 +135,29 @@
       Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
 
     fun pretty_finals reds = Pretty.block
-      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds));
+      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_node o fst) reds));
 
     fun pretty_reduct (lhs, rhs) = Pretty.block
-      ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @
-        Pretty.commas (map prt_const' (sort_by #1 rhs)));
+      ([prt_node lhs, Pretty.str "  ->", Pretty.brk 2] @
+        Pretty.commas (map prt_node ((sort_node_wrt #1) rhs)));
 
     fun pretty_restrict (const, name) =
-      Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
+      Pretty.block ([prt_node const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
     val tsig = Sign.tsig_of thy;
     val consts = Sign.consts_of thy;
     val {const_space, constants, constraints} = Consts.dest consts;
-    val extern_const = Name_Space.extern ctxt const_space;
     val {classes, default, types, ...} = Type.rep_tsig tsig;
+    val type_space = Type.type_space tsig;
     val (class_space, class_algebra) = classes;
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
+    fun extern_node (Defs.NConst c) = Defs.NConst (Name_Space.extern ctxt const_space c)
+      | extern_node (Defs.NType t) = Defs.NType (Name_Space.extern ctxt type_space t);
+
     val clsses =
       Name_Space.extern_entries verbose ctxt class_space
         (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
@@ -163,6 +167,11 @@
       Name_Space.extern_entries verbose ctxt (Type.type_space tsig) (Symtab.dest arities)
       |> map (apfst #1);
 
+    fun prune_const c = not verbose andalso Consts.is_concealed consts c;
+
+    fun prune_node (Defs.NConst c) = prune_const c
+      | prune_node (Defs.NType t) = not verbose andalso Name_Space.is_concealed type_space t;
+
     val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
@@ -170,14 +179,13 @@
 
     val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
 
-    fun prune_const c = not verbose andalso Consts.is_concealed consts c;
-    val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
+    val (reds0, (reds1, reds2)) = filter_out (prune_node o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
-        (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
-      |> sort_by (#1 o #1)
+        (apfst extern_node lhs, map (apfst extern_node) (filter_out (prune_node o fst) rhs)))
+      |> sort_node_wrt (#1 o #1)
       |> List.partition (null o #2)
       ||> List.partition (Defs.plain_args o #2 o #1);
-    val rests = restricts |> map (apfst (apfst extern_const)) |> sort_by (#1 o #1);
+    val rests = restricts |> map (apfst (apfst extern_node)) |> sort_node_wrt (#1 o #1);
   in
     [Pretty.strs ("names:" :: Context.display_names thy)] @
     [Pretty.big_list "classes:" (map pretty_classrel clsses),