# HG changeset patch
# User nipkow
# Date 900338662 -7200
# Node ID 42a7fe39a63a97c334dc6b6ec24e81235df47f4e
# Parent  24f992a25adcc43c2b552faf67a054f648a59893
swapped condition in update_apply.

diff -r 24f992a25adc -r 42a7fe39a63a src/HOL/Update.ML
--- a/src/HOL/Update.ML	Sun Jul 12 11:49:17 1998 +0200
+++ b/src/HOL/Update.ML	Mon Jul 13 16:04:22 1998 +0200
@@ -20,7 +20,7 @@
 
 AddIffs [refl RS update_idem];
 
-Goal "(f(x:=y))z = (if x=z then y else f z)";
+Goal "(f(x:=y))z = (if z=x then y else f z)";
 by (simp_tac (simpset() addsimps [update_def]) 1);
 qed "update_apply";
 Addsimps [update_apply];