src/Pure/display.ML
changeset 4782 9c0b31da51c6
parent 4498 a088ec3e4f5e
child 4950 226f2cde9f4d
     1.1 --- a/src/Pure/display.ML	Fri Apr 03 14:36:05 1998 +0200
     1.2 +++ b/src/Pure/display.ML	Fri Apr 03 14:36:20 1998 +0200
     1.3 @@ -166,7 +166,7 @@
     1.4    in
     1.5      Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg));
     1.6      Pretty.writeln (Pretty.strs ("data:" :: Sign.data_kinds data));
     1.7 -    Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
     1.8 +    Pretty.writeln (Pretty.strs ["name prefix:", NameSpace.pack path]);
     1.9      Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces'));
    1.10      Pretty.writeln (pretty_classes classes);
    1.11      Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel));
    1.12 @@ -192,7 +192,7 @@
    1.13    in
    1.14      Pretty.writeln (Pretty.big_list "axioms:" (map prt_axm axioms));
    1.15      Pretty.writeln (Pretty.strs ("oracles:" :: oras));
    1.16 -    print_data thy "theorems"
    1.17 +    print_data thy "Pure/theorems"	(*forward reference!*)
    1.18    end;
    1.19  
    1.20  fun print_theory thy = (print_sign (sign_of thy); print_thy thy);