added add_del_args;

--- a/src/Pure/Isar/attrib.ML	Fri Mar 31 18:10:21 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Mar 31 21:54:50 2000 +0200
@@ -32,6 +32,7 @@
   val local_thmss: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
   val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
   val no_args: 'a attribute -> Args.src -> 'a attribute
+  val add_del_args: 'a attribute -> 'a attribute -> Args.src -> 'a attribute
   val setup: (theory -> theory) list
 end;
 
@@ -162,6 +163,9 @@
 
 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;
+
 
 
 (** Pure attributes **)