--- 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));