# HG changeset patch
# User wenzelm
# Date 916157953 -3600
# Node ID 1418bc571f2312d3322feb0e763d4daccd6b5f95
# Parent  f5999c0f40b9dddafea44f7beef45a438066e8e9
tuned msg;

diff -r f5999c0f40b9 -r 1418bc571f23 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jan 12 17:17:07 1999 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jan 12 17:19:13 1999 +0100
@@ -84,7 +84,7 @@
       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     val (int_cmds, cmds) = partition (#1 o #2 o #2) (Symtab.dest (! global_parsers));
   in
-    Pretty.writeln (Pretty.strs ("keywords:" :: map quote keywords));
+    Pretty.writeln (Pretty.strs ("syntax keywords:" :: map quote keywords));
     Pretty.writeln (Pretty.big_list "proper commands:" (map pretty_cmd cmds));
     Pretty.writeln (Pretty.big_list "improper commands (interactive-only):"
       (map pretty_cmd int_cmds))