# HG changeset patch
# User paulson
# Date 900415915 -7200
# Node ID 495a4f9af897070ed58e7adb06931dd77601e058
# Parent  216a5dab14b68de2cb4b6239701c28269f10936b
CHANGED_GOAL added to declare a more robust stac

diff -r 216a5dab14b6 -r 495a4f9af897 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Tue Jul 14 13:30:01 1998 +0200
+++ b/src/Pure/tctical.ML	Tue Jul 14 13:31:55 1998 +0200
@@ -19,6 +19,7 @@
   val APPEND            : tactic * tactic -> tactic
   val APPEND'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val CHANGED           : tactic -> tactic
+  val CHANGED_GOAL	: (int -> tactic) -> int -> tactic
   val COND              : (thm -> bool) -> tactic -> tactic -> tactic   
   val DETERM            : tactic -> tactic
   val EVERY             : tactic list -> tactic   
@@ -57,7 +58,7 @@
   val THEN_ALL_NEW	: (int -> tactic) * (int -> tactic) -> int -> tactic
   val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
   val traced_tac        : (thm -> (thm * thm Seq.seq) option) -> tactic
-  val tracify           : bool ref -> tactic -> thm -> thm Seq.seq
+  val tracify           : bool ref -> tactic -> tactic
   val trace_REPEAT      : bool ref
   val TRY               : tactic -> tactic
   val TRYALL            : (int -> tactic) -> tactic   
@@ -323,6 +324,18 @@
 fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i-1),  i) st
                              handle Subscript => Seq.empty;
 
+(*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
+        val t = List.nth(prems_of st, i-1)
+        fun diff st' = 
+	    not (nprems_of st' > j   (*subgoal is still there*)
+		 andalso
+		 t aconv List.nth(prems_of st', nprems_of st' - j - 1))
+    in  Seq.filter diff (tac i st)  end
+    handle Subscript => Seq.empty  (*no subgoal i*);
+
 fun ALLGOALS_RANGE tac (i:int) j st =
   if i > j then all_tac st
   else (tac j THEN ALLGOALS_RANGE tac i (j - 1)) st;