author | paulson |
Thu, 04 Apr 1996 12:58:47 +0200 | |
changeset 1643 | 3f83b629f2e3 |
parent 1642 | 21db0cf9a1a4 |
child 1644 | 681f70ca3cf7 |
--- 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 ***)