changeset 1643 | 3f83b629f2e3 |
parent 1583 | bc902840aab5 |
child 2005 | a52f53caf424 |
--- a/src/Pure/tctical.ML Thu Apr 04 11:45:01 1996 +0200 +++ b/src/Pure/tctical.ML Thu Apr 04 12:58:47 1996 +0200 @@ -265,11 +265,9 @@ fun FILTER pred tac st = Sequence.filters pred (tac st); (*Returns all changed states*) -fun CHANGED tac = - (fn st => - let fun diff st = not (eq_thm(st,st)) - in Sequence.filters diff (tac st) - end ); +fun CHANGED tac st = + let fun diff st' = not (eq_thm(st,st')) + in Sequence.filters diff (tac st) end; (*** Tacticals based on subgoal numbering ***)