tactical CHANGED now uses alpha-eta conversion, not alpha conversion
authorpaulson
Mon Nov 30 10:45:39 1998 +0100 (1998-11-30)
changeset 59974d00bbd3d3ac
parent 5996 6b6e0ede3517
child 5998 b2ecd577b8a3
tactical CHANGED now uses alpha-eta conversion, not alpha conversion

Streamlined code
src/Pure/tctical.ML
     1.1 --- a/src/Pure/tctical.ML	Mon Nov 30 10:44:05 1998 +0100
     1.2 +++ b/src/Pure/tctical.ML	Mon Nov 30 10:45:39 1998 +0100
     1.3 @@ -327,12 +327,13 @@
     1.4  (*Returns all states that have changed in subgoal i, counted from the LAST
     1.5    subgoal.  For stac, for example.*)
     1.6  fun CHANGED_GOAL tac i st = 
     1.7 -    let val j = nprems_of st - i
     1.8 +    let val j = nprems_of st
     1.9          val t = List.nth(prems_of st, i-1)
    1.10 -        fun diff st' = 
    1.11 -	    not (nprems_of st' > j   (*subgoal is still there*)
    1.12 +        fun diff st' = (*true if subgoal still exists and is same as old one*)
    1.13 +	    not (nprems_of st' >= j
    1.14  		 andalso
    1.15 -		 t aconv List.nth(prems_of st', nprems_of st' - j - 1))
    1.16 +		 Pattern.aeconv (t,
    1.17 +				 List.nth(prems_of st', nprems_of st' - j)))
    1.18      in  Seq.filter diff (tac i st)  end
    1.19      handle Subscript => Seq.empty  (*no subgoal i*);
    1.20