Proved and added rewrite rule (@x. x=y) = y to simpset.
Strange that only the symetric version was present!

--- a/src/HOL/HOL.ML	Wed Sep 09 17:25:49 1998 +0200
+++ b/src/HOL/HOL.ML	Wed Sep 09 17:34:58 1998 +0200
@@ -297,7 +297,12 @@
         etac exE 1,
         etac selectI 1]);
 
-qed_goal "Eps_eq" HOL.thy "(Eps (op = x)) = x" (K [
+qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [
+	rtac select_equality 1,
+	rtac refl 1,
+	atac 1]);
+
+qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [
 	rtac select_equality 1,
 	rtac refl 1,
 	etac sym 1]);

--- a/src/HOL/simpdata.ML	Wed Sep 09 17:25:49 1998 +0200
+++ b/src/HOL/simpdata.ML	Wed Sep 09 17:34:58 1998 +0200
@@ -420,7 +420,7 @@
        if_True, if_False, if_cancel, if_eq_cancel,
        imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
-       disj_not1, not_all, not_ex, cases_simp, Eps_eq]
+       disj_not1, not_all, not_ex, cases_simp, Eps_eq, Eps_sym_eq]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]
      addcongs [imp_cong]