# HG changeset patch
# User paulson
# Date 912419139 -3600
# Node ID 4d00bbd3d3acd2f9372d45e94ff750e3fbb1234e
# Parent  6b6e0ede35174ed6a3425c2e6afe82385131a361
tactical CHANGED now uses alpha-eta conversion, not alpha conversion

Streamlined code

diff -r 6b6e0ede3517 -r 4d00bbd3d3ac src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Mon Nov 30 10:44:05 1998 +0100
+++ b/src/Pure/tctical.ML	Mon Nov 30 10:45:39 1998 +0100
@@ -327,12 +327,13 @@
 (*Returns all states that have changed in subgoal i, counted from the LAST
   subgoal.  For stac, for example.*)
 fun CHANGED_GOAL tac i st = 
-    let val j = nprems_of st - i
+    let val j = nprems_of st
         val t = List.nth(prems_of st, i-1)
-        fun diff st' = 
-	    not (nprems_of st' > j   (*subgoal is still there*)
+        fun diff st' = (*true if subgoal still exists and is same as old one*)
+	    not (nprems_of st' >= j
 		 andalso
-		 t aconv List.nth(prems_of st', nprems_of st' - j - 1))
+		 Pattern.aeconv (t,
+				 List.nth(prems_of st', nprems_of st' - j)))
     in  Seq.filter diff (tac i st)  end
     handle Subscript => Seq.empty  (*no subgoal i*);