afford strict check (see also AFP/a8e08d947f0a);
authorwenzelm
Tue May 20 20:05:43 2014 +0200 (2014-05-20)
changeset 5702690a3e39be0ca
parent 57025 e7fd64f82876
child 57027 80ffda443738
afford strict check (see also AFP/a8e08d947f0a);
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue May 20 19:24:39 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue May 20 20:05:43 2014 +0200
     1.3 @@ -157,20 +157,14 @@
     1.4            then Keyword.define (name, SOME kind)
     1.5            else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
     1.6      val _ = Context_Position.report_generic context pos (command_markup true (name, cmd));
     1.7 -
     1.8 -    fun redefining () =
     1.9 -      "Redefining outer syntax command " ^ quote name ^ Position.here (Position.thread_data ());
    1.10    in
    1.11      Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
    1.12       (if not (Symtab.defined commands name) then ()
    1.13 +      else if ! batch_mode then
    1.14 +        error ("Attempt to redefine outer syntax command " ^ quote name)
    1.15        else
    1.16 -        let
    1.17 -          val _ = warning (redefining ());
    1.18 -          val _ =
    1.19 -            if ! batch_mode then
    1.20 -              Output.physical_stderr ("### Legacy feature!! " ^ redefining () ^ "\n")
    1.21 -            else ();
    1.22 -        in () end;
    1.23 +        warning ("Redefining outer syntax command " ^ quote name ^
    1.24 +          Position.here (Position.thread_data ()));
    1.25        Symtab.update (name, cmd) commands)))
    1.26    end);
    1.27