tuned msg;
authorwenzelm
Thu, 01 Dec 2005 22:03:05 +0100
changeset 18326 2f57579e618f
parent 18325 2d504ea54e5b
child 18327 1ee4523c831f
tuned msg;
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;