# HG changeset patch
# User wenzelm
# Date 1399890693 -7200
# Node ID ef44b488bad8ab9f85e011282b11b2a48b6555ad
# Parent  d11d11da0d904d7506ab3c7843e28423dcfaa6f1
tuned message;

diff -r d11d11da0d90 -r ef44b488bad8 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon May 12 12:01:02 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon May 12 12:31:33 2014 +0200
@@ -168,7 +168,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)))