src/Pure/tctical.ML
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 ***)