# 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 "(){}[],";