# HG changeset patch
# User wenzelm
# Date 1400609143 -7200
# Node ID 90a3e39be0ca1dbc4a3dc9768d9457581205adbf
# Parent  e7fd64f828760fb1c717fb5086bf86ed430b0335
afford strict check (see also AFP/a8e08d947f0a);

diff -r e7fd64f82876 -r 90a3e39be0ca src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue May 20 19:24:39 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue May 20 20:05:43 2014 +0200
@@ -157,20 +157,14 @@
           then Keyword.define (name, SOME kind)
           else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
     val _ = Context_Position.report_generic context pos (command_markup true (name, cmd));
-
-    fun redefining () =
-      "Redefining outer syntax command " ^ quote name ^ Position.here (Position.thread_data ());
   in
     Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
      (if not (Symtab.defined commands name) then ()
+      else if ! batch_mode then
+        error ("Attempt to redefine outer syntax command " ^ quote name)
       else
-        let
-          val _ = warning (redefining ());
-          val _ =
-            if ! batch_mode then
-              Output.physical_stderr ("### Legacy feature!! " ^ redefining () ^ "\n")
-            else ();
-        in () end;
+        warning ("Redefining outer syntax command " ^ quote name ^
+          Position.here (Position.thread_data ()));
       Symtab.update (name, cmd) commands)))
   end);