diff -r 5610c4acb48d -r 24914e42b857 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Sep 13 22:31:19 2000 +0200
@@ -156,8 +156,8 @@
 
 fun no_args x = syntax (Scan.succeed x);
 
-fun add_del_args add del x =
-  syntax (Scan.lift (Args.$$$ "add" >> K add || Args.$$$ "del" >> K del || Scan.succeed add)) x;
+fun add_del_args add del x = syntax (Scan.lift
+    (Args.$$$ Args.addN >> K add || Args.$$$ Args.delN >> K del || Scan.succeed add)) x;