# HG changeset patch
# User paulson
# Date 828615527 -7200
# Node ID 3f83b629f2e37a2bbf2f1c21ab152aee88f3dab3
# Parent  21db0cf9a1a41791acc744a69d4e97bbef457151
Fixed error in CHANGED (caused by variable renaming)

diff -r 21db0cf9a1a4 -r 3f83b629f2e3 src/Pure/tctical.ML
--- 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 ***)