# HG changeset patch
# User wenzelm
# Date 954532490 -7200
# Node ID 427ead639d8ae6288c10f3ba83960144067d9a81
# Parent  14a69a0e86792e4740622e27ac185937183b3f65
added add_del_args;

diff -r 14a69a0e8679 -r 427ead639d8a src/Pure/Isar/attrib.ML
--- 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 **)