src/Pure/Isar/outer_syntax.ML
changeset 16894 40f80823b451
parent 16727 e264077b68a7
child 17071 f753d6dd9bd0
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 19 20:47:00 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 19 20:47:01 2005 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4    (Scan.extend_lexicon lex (map Symbol.explode keywords))));
     1.5  
     1.6  fun add_parser (tab, Parser (name, (comment, kind, markup), int_only, parse)) =
     1.7 - (if is_none (Symtab.lookup (tab, name)) then ()
     1.8 + (if not (Symtab.defined tab name) then ()
     1.9    else warning ("Redefined outer syntax command " ^ quote name);
    1.10    Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
    1.11