# HG changeset patch
# User wenzelm
# Date 1235748791 -3600
# Node ID 09817540ccae17d9effa6f8ae2302ae3e9ae637e
# Parent  56ae4893e8ae3f056ecdddb6801d8be974da7776
tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;

diff -r 56ae4893e8ae -r 09817540ccae src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Fri Feb 27 16:18:02 2009 +0100
+++ b/src/Pure/tctical.ML	Fri Feb 27 16:33:11 2009 +0100
@@ -349,15 +349,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 np = nprems_of st
+    let val np = Thm.nprems_of st
         val d = np-i                 (*distance from END*)
-        val t = List.nth(prems_of st, i-1)
+        val t = Thm.term_of (Thm.cprem_of st i)
         fun diff st' =
-            nprems_of st' - d <= 0   (*the subgoal no longer exists*)
+            Thm.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)))
+             not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
     in  Seq.filter diff (tac i st)  end
     handle Subscript => Seq.empty  (*no subgoal i*);