| changeset 9952 | 24914e42b857 |
| parent 9941 | fe05af7ec816 |
| child 10034 | 4bca6b2d2589 |
--- 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;