src/Pure/Isar/method.ML
changeset 9777 232fb8886765
parent 9706 8e48a19fc81e
child 9864 b4a170f7d658
     1.1 --- a/src/Pure/Isar/method.ML	Fri Sep 01 00:33:14 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Fri Sep 01 00:33:36 2000 +0200
     1.3 @@ -75,6 +75,10 @@
     1.4    val bang_sectioned_args:
     1.5      (Args.T list -> modifier * Args.T list) list ->
     1.6      (thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
     1.7 +  val bang_sectioned_args':
     1.8 +    (Args.T list -> modifier * Args.T list) list ->
     1.9 +    (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.10 +    ('a -> thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.11    val only_sectioned_args:
    1.12      (Args.T list -> modifier * Args.T list) list ->
    1.13      (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.14 @@ -507,6 +511,8 @@
    1.15    in f x ctxt' end;
    1.16  
    1.17  fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
    1.18 +fun bang_sectioned_args' ss scan f =
    1.19 +  sectioned_args (Args.bang_facts -- scan >> swap) ss (uncurry f);
    1.20  fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f);
    1.21  
    1.22  fun thms_ctxt_args f = sectioned_args (thmss []) [] f;