# HG changeset patch
# User paulson
# Date 939025158 -7200
# Node ID 4731f10af2e60d66644559ce94aad731fd6e523e
# Parent  3edd32d588a6463f7ba8f3042e1aa42304b85bfa
fixed CHANGED_GOAL, which is used by stac

diff -r 3edd32d588a6 -r 4731f10af2e6 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Sun Oct 03 15:54:25 1999 +0200
+++ b/src/Pure/tctical.ML	Mon Oct 04 10:19:18 1999 +0200
@@ -328,13 +328,15 @@
 (*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
+    let val np = nprems_of st
+        val d = np-i                 (*distance from END*)
         val t = List.nth(prems_of st, i-1)
-        fun diff st' = (*true if subgoal still exists and is same as old one*)
-	    not (nprems_of st' >= j
-		 andalso
-		 Pattern.aeconv (t,
-				 List.nth(prems_of st', nprems_of st' - j)))
+        fun diff st' = 
+	    nprems_of st' - d <= 0   (*the subgoal no longer exists*)
+	    orelse 
+             not (Pattern.aeconv (t,
+				  List.nth(prems_of st', 
+					   nprems_of st' - d - 1)))
     in  Seq.filter diff (tac i st)  end
     handle Subscript => Seq.empty  (*no subgoal i*);