diff -r a8f5611dbd65 -r 135ac0fb2686 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Fri Oct 15 23:45:54 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Sun Oct 17 13:35:52 2010 +0100
@@ -28,11 +28,11 @@
 lemma permute_fset[simp, eqvt]:
   fixes S::"('a::pt) fset"
   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
-  and   "(p \<bullet> finsert x S) = finsert (p \<bullet> x) (p \<bullet> S)"
+  and   "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
-lemma fmap_eqvt[eqvt]: 
-  shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
+lemma map_fset_eqvt[eqvt]: 
+  shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
 
 lemma fset_eqvt[eqvt]: 
@@ -44,15 +44,15 @@
   unfolding supp_def
   by (perm_simp) (simp add: fset_cong)
 
-lemma supp_fempty [simp]:
+lemma supp_empty_fset [simp]:
   shows "supp {||} = {}"
   unfolding supp_def
   by simp
 
-lemma supp_finsert [simp]:
+lemma supp_insert_fset [simp]:
   fixes x::"'a::fs"
   and   S::"'a fset"
-  shows "supp (finsert x S) = supp x \<union> supp S"
+  shows "supp (insert_fset x S) = supp x \<union> supp S"
   apply(subst supp_fset[symmetric])
   apply(simp add: supp_fset supp_of_fin_insert)
   done
@@ -70,25 +70,25 @@
   apply (rule fset_finite_supp)
   done
 
-lemma atom_fmap_cong:
-  shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y"
-  apply(rule inj_fmap_eq_iff)
+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(simp add: inj_on_def)
   done
 
-lemma supp_fmap_atom:
-  shows "supp (fmap atom S) = supp S"
+lemma supp_map_fset_atom:
+  shows "supp (map_fset atom S) = supp S"
   unfolding supp_def
   apply(perm_simp)
-  apply(simp add: atom_fmap_cong)
+  apply(simp add: atom_map_fset_cong)
   done
 
 lemma supp_at_fset:
   fixes S::"('a::at_base) fset"
-  shows "supp S = fset (fmap atom S)"
+  shows "supp S = fset (map_fset atom S)"
   apply (induct S)
-  apply (simp add: supp_fempty)
-  apply (simp add: supp_finsert)
+  apply (simp add: supp_empty_fset)
+  apply (simp add: supp_insert_fset)
   apply (simp add: supp_at_base)
   done