diff -r d7269488c4b5 -r 1f5c8e85c41f Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Sun Oct 17 15:28:05 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Sun Oct 17 15:53:37 2010 +0100
@@ -72,7 +72,7 @@
 
 lemma atom_map_fset_cong:
   shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"
-  apply(rule inj_map_fset_eq_iff)
+  apply(rule inj_map_fset_cong)
   apply(simp add: inj_on_def)
   done