# HG changeset patch
# User wenzelm
# Date 1133470985 -3600
# Node ID 2f57579e618f2b18f0a2ee594852f0729b66d414
# Parent  2d504ea54e5b4a14d8fde233d18eb17cbbdd9d1e
tuned msg;

diff -r 2d504ea54e5b -r 2f57579e618f src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Dec 01 22:03:04 2005 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Dec 01 22:03:05 2005 +0100
@@ -172,8 +172,8 @@
     val (int_cmds, cmds) = List.partition #4 (dest_parsers ());
   in
     [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
-      Pretty.big_list "proper commands:" (map pretty_cmd cmds),
-      Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)]
+      Pretty.big_list "commands:" (map pretty_cmd cmds),
+      Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
     |> Pretty.chunks |> Pretty.writeln
   end;