# HG changeset patch
# User wenzelm
# Date 947069017 -3600
# Node ID d5eb246c94ec05f67b621296ba5975a37fab776b
# Parent  badbfb6ceac0520308aa4fb7173bd9f3b43f7691
added thms_ctxt_args;

diff -r badbfb6ceac0 -r d5eb246c94ec src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Jan 05 11:43:09 2000 +0100
+++ b/src/Pure/Isar/method.ML	Wed Jan 05 11:43:37 2000 +0100
@@ -49,6 +49,8 @@
   val only_sectioned_args:
     (Args.T list -> modifier * Args.T list) list ->
     (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+  val thms_ctxt_args: (thm list -> Proof.context -> Proof.method)
+    -> Args.src -> Proof.context -> Proof.method
   val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
   datatype text =
     Basic of (Proof.context -> Proof.method) |
@@ -297,7 +299,8 @@
 fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
 fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f);
 
-fun thms_args f = sectioned_args (thmss []) [] (fn ths => fn _ => f ths);
+fun thms_ctxt_args f = sectioned_args (thmss []) [] f;
+fun thms_args f = thms_ctxt_args (K o f);
 
 end;