--- a/src/Pure/tctical.ML Tue Oct 15 15:37:57 2002 +0200
+++ b/src/Pure/tctical.ML Thu Oct 17 10:52:59 2002 +0200
@@ -291,10 +291,13 @@
fun FILTER pred tac st = Seq.filter pred (tac st);
+(*Accept only next states that change the theorem somehow*)
fun CHANGED tac st =
let fun diff st' = not (Thm.eq_thm (st, st'));
in Seq.filter diff (tac st) end;
+(*Accept only next states that change the theorem's prop field
+ (changes to signature, hyps, etc. don't count)*)
fun CHANGED_PROP tac st =
let fun diff st' = not (Drule.eq_thm_prop (st, st'));
in Seq.filter diff (tac st) end;