# HG changeset patch
# User wenzelm
# Date 1007518437 -3600
# Node ID 86c58273f8c0df6391fd0393e9a815264ce7fd0f
# Parent  c1e3e7d3f469f68ee6c5f801b8c378acd36ef3a3
removed bang_args;

diff -r c1e3e7d3f469 -r 86c58273f8c0 src/Pure/Isar/attrib.ML
--- 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;