# 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*);