tuned message;
authorwenzelm
Mon, 12 May 2014 12:31:33 +0200
changeset 56938 ef44b488bad8
parent 56937 d11d11da0d90
child 56939 c2ddbf327bbd
tuned message;
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)))