# HG changeset patch
# User wenzelm
# Date 1392385483 -3600
# Node ID c12ad7295f57a0e09d9a00c7777d0d6ed16cacbc
# Parent  60c159d490a210430d1436ac9b75dd2fcb941d29
tuned message;

diff -r 60c159d490a2 -r c12ad7295f57 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Feb 14 14:39:44 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Feb 14 14:44:43 2014 +0100
@@ -167,7 +167,7 @@
           val _ = warning (redefining ());
           val _ =
             if ! batch_mode then
-              Output.physical_stderr ("Legacy feature! " ^ redefining () ^ "\n")
+              Output.physical_stderr ("### Legacy feature! " ^ redefining () ^ "\n")
             else ();
         in () end;
       Symtab.update (name, cmd) commands)))