--- a/src/Pure/Isar/args.ML Tue Sep 21 14:21:53 1999 +0200
+++ b/src/Pure/Isar/args.ML Tue Sep 21 17:06:49 1999 +0200
@@ -36,6 +36,7 @@
val local_prop: Proof.context * T list -> term * (Proof.context * T list)
val local_term_pat: Proof.context * T list -> term * (Proof.context * T list)
val local_prop_pat: Proof.context * T list -> term * (Proof.context * T list)
+ val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
type src
val src: (string * T list) * Position.T -> src
val dest_src: src -> (string * T list) * Position.T
@@ -140,6 +141,12 @@
val local_prop_pat = gen_item ProofContext.read_prop_pat;
+(* bang facts *)
+
+val bang_facts = Scan.depend (fn ctxt =>
+ ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
+
+
(* args *)
val exclude = explode "(){}[],";