# HG changeset patch
# User wenzelm
# Date 937926409 -7200
# Node ID af3a1fe87c428a9ba9587620eda2ff3e8a7a23a4
# Parent  0d6d1f50b86dcc7784548e6e9caba2a3e975a927
added bang_facts;

diff -r 0d6d1f50b86d -r af3a1fe87c42 src/Pure/Isar/args.ML
--- 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 "(){}[],";