# HG changeset patch
# User wenzelm
# Date 1182287751 -7200
# Node ID b2d64f86d21b66b8b98694846bba395740d96b5c
# Parent  4a368c087f58ff671c2fe30499dab7869ece6710
added with_subgoal;

diff -r 4a368c087f58 -r b2d64f86d21b src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jun 19 23:15:49 2007 +0200
+++ b/src/Pure/drule.ML	Tue Jun 19 23:15:51 2007 +0200
@@ -119,6 +119,7 @@
   val term_rule: theory -> (thm -> thm) -> term -> term
   val sort_triv: theory -> typ * sort -> thm list
   val unconstrainTs: thm -> thm
+  val with_subgoal: int -> (thm -> thm) -> thm -> thm
   val rename_bvars: (string * string) list -> thm -> thm
   val rename_bvars': string option list -> thm -> thm
   val incr_indexes: thm -> thm -> thm
@@ -443,6 +444,7 @@
 
 (*Rotates a rule's premises to the left by k*)
 val rotate_prems = permute_prems 0;
+fun with_subgoal i f = rotate_prems (i - 1) #> f #> rotate_prems (1 - i);
 
 (* permute prems, where the i-th position in the argument list (counting from 0)
    gives the position within the original thm to be transferred to position i.