--- a/Nominal/FSet.thy	Sun Oct 17 15:28:05 2010 +0100
+++ b/Nominal/FSet.thy	Sun Oct 17 15:53:37 2010 +0100
@@ -747,7 +747,7 @@
   shows "fset (map_fset f S) = f ` (fset S)"
   by (descending) (simp)
 
-lemma nj_map_fset_cong:
+lemma inj_map_fset_cong:
   shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T"
   by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)
 

--- 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
 

--- a/Nominal/nominal_dt_rawfuns.ML	Sun Oct 17 15:28:05 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Sun Oct 17 15:53:37 2010 +0100
@@ -101,7 +101,7 @@
     val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
     val fset = @{term "fset :: atom fset => atom set"}
   in
-    fset $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+    fset $ (Const (@{const_name map_fset}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
   end
 
   fun mk_atom_list t =