diff -r 0cc94e6f6ae5 -r 40f80823b451 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 19 20:47:00 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 19 20:47:01 2005 +0200
@@ -198,7 +198,7 @@
   (Scan.extend_lexicon lex (map Symbol.explode keywords))));
 
 fun add_parser (tab, Parser (name, (comment, kind, markup), int_only, parse)) =
- (if is_none (Symtab.lookup (tab, name)) then ()
+ (if not (Symtab.defined tab name) then ()
   else warning ("Redefined outer syntax command " ^ quote name);
   Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));