src/Pure/goal.ML
changeset 19221 aab0c0399e91
parent 19191 56cda3ec2ef8
child 19423 51eeee99bd8f
     1.1 --- a/src/Pure/goal.ML	Wed Mar 08 18:37:25 2006 +0100
     1.2 +++ b/src/Pure/goal.ML	Wed Mar 08 18:37:27 2006 +0100
     1.3 @@ -179,10 +179,10 @@
     1.4     else Seq.single (foldr1 Drule.mk_conjunction (map (Thm.cprem_of st) (i upto (i + n - 1)))))
     1.5    |> Seq.map (Thm.adjust_maxidx #> init);
     1.6  
     1.7 -fun retrofit i n st' =
     1.8 -  (if n = 1 then I
     1.9 -   else Drule.rotate_prems (i - 1) #> Drule.conj_uncurry n #> Drule.rotate_prems (1 - i))
    1.10 -  #> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
    1.11 +fun retrofit i n st' st =
    1.12 +  (if n = 1 then st
    1.13 +   else st |> Drule.rotate_prems (i - 1) |> Drule.conj_uncurry n |> Drule.rotate_prems (1 - i))
    1.14 +  |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
    1.15  
    1.16  fun SELECT_GOAL tac i st =
    1.17    if Thm.nprems_of st = 1 andalso i = 1 then tac st