--- 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;