diff -r fd0f737b1956 -r 9f75a45384dd src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jan 12 15:18:47 1999 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jan 12 15:19:09 1999 +0100
@@ -85,8 +85,9 @@
     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.big_list "general commands:" (map pretty_cmd cmds));
-    Pretty.writeln (Pretty.big_list "interactive commands:" (map pretty_cmd int_cmds))
+    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))
   end;