SELECT_GOAL: fixed trivial case;
authorwenzelm
Sun Mar 05 23:56:57 2006 +0100 (2006-03-05)
changeset 1919156cda3ec2ef8
parent 19190 7c311c513bae
child 19192 ee5fde055c9a
SELECT_GOAL: fixed trivial case;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Sun Mar 05 18:49:13 2006 +0100
     1.2 +++ b/src/Pure/goal.ML	Sun Mar 05 23:56:57 2006 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4    #> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
     1.5  
     1.6  fun SELECT_GOAL tac i st =
     1.7 -  if Thm.nprems_of st = 1 then tac st
     1.8 +  if Thm.nprems_of st = 1 andalso i = 1 then tac st
     1.9    else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
    1.10  
    1.11  end;