# HG changeset patch # User wenzelm # Date 967761216 -7200 # Node ID 232fb8886765be5f9a4559162750f47c840a135a # Parent a126bc3b73762962b852d88da2bdcccdd1746ae8 added bang_sectioned_args'; 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;