src/Pure/Isar/method.ML
changeset 8093 d5eb246c94ec
parent 7664 c151ac595551
child 8153 9bdbcb71dc56
     1.1 --- a/src/Pure/Isar/method.ML	Wed Jan 05 11:43:09 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Jan 05 11:43:37 2000 +0100
     1.3 @@ -49,6 +49,8 @@
     1.4    val only_sectioned_args:
     1.5      (Args.T list -> modifier * Args.T list) list ->
     1.6      (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
     1.7 +  val thms_ctxt_args: (thm list -> Proof.context -> Proof.method)
     1.8 +    -> Args.src -> Proof.context -> Proof.method
     1.9    val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.10    datatype text =
    1.11      Basic of (Proof.context -> Proof.method) |
    1.12 @@ -297,7 +299,8 @@
    1.13  fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
    1.14  fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f);
    1.15  
    1.16 -fun thms_args f = sectioned_args (thmss []) [] (fn ths => fn _ => f ths);
    1.17 +fun thms_ctxt_args f = sectioned_args (thmss []) [] f;
    1.18 +fun thms_args f = thms_ctxt_args (K o f);
    1.19  
    1.20  end;
    1.21