# HG changeset patch
# User wenzelm
# Date 1141839447 -3600
# Node ID aab0c0399e91b7a0bede6fbd504e337f7642b05d
# Parent  05b00acff957ea0dddd35ef4ea04b99647c15440
tuned;

diff -r 05b00acff957 -r aab0c0399e91 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Mar 08 18:37:25 2006 +0100
+++ b/src/Pure/goal.ML	Wed Mar 08 18:37:27 2006 +0100
@@ -179,10 +179,10 @@
    else Seq.single (foldr1 Drule.mk_conjunction (map (Thm.cprem_of st) (i upto (i + n - 1)))))
   |> Seq.map (Thm.adjust_maxidx #> init);
 
-fun retrofit i n st' =
-  (if n = 1 then I
-   else Drule.rotate_prems (i - 1) #> Drule.conj_uncurry n #> Drule.rotate_prems (1 - i))
-  #> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
+fun retrofit i n st' st =
+  (if n = 1 then st
+   else st |> Drule.rotate_prems (i - 1) |> Drule.conj_uncurry n |> Drule.rotate_prems (1 - i))
+  |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
 
 fun SELECT_GOAL tac i st =
   if Thm.nprems_of st = 1 andalso i = 1 then tac st