diff -r a126bc3b7376 -r 232fb8886765 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Sep 01 00:33:14 2000 +0200
+++ b/src/Pure/Isar/method.ML	Fri Sep 01 00:33:36 2000 +0200
@@ -75,6 +75,10 @@
   val bang_sectioned_args:
     (Args.T list -> modifier * Args.T list) list ->
     (thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+  val bang_sectioned_args':
+    (Args.T list -> modifier * Args.T list) list ->
+    (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
+    ('a -> thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
   val only_sectioned_args:
     (Args.T list -> modifier * Args.T list) list ->
     (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
@@ -507,6 +511,8 @@
   in f x ctxt' end;
 
 fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
+fun bang_sectioned_args' ss scan f =
+  sectioned_args (Args.bang_facts -- scan >> swap) ss (uncurry f);
 fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f);
 
 fun thms_ctxt_args f = sectioned_args (thmss []) [] f;