removed bang_args;

--- a/src/Pure/Isar/attrib.ML	Wed Dec 05 03:13:21 2001 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Dec 05 03:13:57 2001 +0100
@@ -32,7 +32,6 @@
   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 bang_args: 'a attribute -> 'a attribute -> Args.src -> 'a attribute
   val add_del_args: 'a attribute -> 'a attribute -> Args.src -> 'a attribute
   val setup: (theory -> theory) list
 end;
@@ -157,9 +156,6 @@
 
 fun no_args x = syntax (Scan.succeed x);
 
-fun bang_args a b x = syntax
-  (Scan.lift Args.bang >> K a || Scan.succeed b) x;
-
 fun add_del_args add del x = syntax
   (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add)) x;