# HG changeset patch
# User wenzelm
# Date 891606980 -7200
# Node ID 9c0b31da51c6f468bc433366eac5c2f4798d480b
# Parent  6b55d02437ade811a72d2bda1714cb5067cb3f63
tuned comments;

diff -r 6b55d02437ad -r 9c0b31da51c6 src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Apr 03 14:36:05 1998 +0200
+++ b/src/Pure/display.ML	Fri Apr 03 14:36:20 1998 +0200
@@ -166,7 +166,7 @@
   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.strs ["name prefix:", NameSpace.pack path]);
     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));
@@ -192,7 +192,7 @@
   in
     Pretty.writeln (Pretty.big_list "axioms:" (map prt_axm axioms));
     Pretty.writeln (Pretty.strs ("oracles:" :: oras));
-    print_data thy "theorems"
+    print_data thy "Pure/theorems"	(*forward reference!*)
   end;
 
 fun print_theory thy = (print_sign (sign_of thy); print_thy thy);