src/Pure/pure_thy.ML
changeset 4498 a088ec3e4f5e
parent 4487 9b4c1db5aca1
child 4590 9f8f931e0089
--- a/src/Pure/pure_thy.ML	Mon Dec 29 14:30:38 1997 +0100
+++ b/src/Pure/pure_thy.ML	Mon Dec 29 14:31:20 1997 +0100
@@ -63,7 +63,7 @@
       if ! long_names then name else NameSpace.extern space name;
     val thmss = sort_wrt fst (map (apfst extrn) (Symtab.dest thms_tab));
   in
-    Pretty.writeln (Pretty.strs ("theorem name space:" :: map quote (NameSpace.dest space)));
+    Pretty.writeln (Display.pretty_name_space ("theorem name space", space));
     Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
   end;