# HG changeset patch
# User wenzelm
# Date 1003170733 -7200
# Node ID e7eeca372b7c7dcfb97df5b202d3d05b1254ee74
# Parent  3bc4f67d7fe11af3fb1b6c2f4f538c60568bd4ab
bang_args;

diff -r 3bc4f67d7fe1 -r e7eeca372b7c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Oct 15 20:31:52 2001 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Oct 15 20:32:13 2001 +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 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;
@@ -156,6 +157,9 @@
 
 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;