src/Pure/display.ML

   val pretty_thm	: thm -> Pretty.T
   val print_cterm	: cterm -> unit
   val print_ctyp	: ctyp -> unit
   val show_consts	: bool ref
   val print_goals	: int -> thm -> unit
+  val pretty_name_space : string * NameSpace.T -> Pretty.T
   val print_syntax	: theory -> unit
   val print_theory	: theory -> unit
   val print_data	: theory -> string -> unit
   val print_thm		: thm -> unit
   val prth		: thm -> thm

 
 val print_syntax = Syntax.print_syntax o syn_of;
 val print_data = Sign.print_data o sign_of;
 
 
+(* pretty_name_space  *)
+
+fun pretty_name_space (kind, space) =
+  let
+    fun prt_entry (name, accs) = Pretty.block
+      (Pretty.str (quote name ^ " =") :: Pretty.brk 1 ::
+        Pretty.commas (map (Pretty.str o quote) accs));
+  in
+    Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space))
+    |> Pretty.block
+  end;
+
+
+
 (* print signature *)
 
 fun print_sign sg =
   let
     fun prt_cls c = Sign.pretty_sort sg [c];

 
     val ext_class = Sign.cond_extern sg Sign.classK;
     val ext_tycon = Sign.cond_extern sg Sign.typeK;
     val ext_const = Sign.cond_extern sg Sign.constK;
 
-
-    fun pretty_space (kind, space) = Pretty.block (Pretty.breaks
-      (map Pretty.str (kind ^ ":" :: map quote (NameSpace.dest space))));
 
     fun pretty_classes cs = Pretty.block
       (Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs));
 
     fun pretty_classrel (c, cs) = Pretty.block

     val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab));
   in
     Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg));
     Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data));
     Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
-    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces'));
+    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces'));
     Pretty.writeln (pretty_classes classes);
     Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel));
     Pretty.writeln (pretty_default default);
     Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons));
     Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr abbrs));