--- a/Nominal/Nominal2_FSet.thy	Wed Apr 21 21:52:30 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Thu Apr 22 05:16:23 2010 +0200
@@ -71,55 +71,6 @@
   apply (simp add: atom_fmap_cong)
   done
 
-lemma supp_atom_insert:
-  "finite (xs :: atom set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs"
-  apply (simp add: supp_finite_atom_set)
-  apply (simp add: supp_atom)
-  done
-
-lemma atom_image_cong:
-  shows "(atom ` X = atom ` Y) = (X = Y)"
-  apply(rule inj_image_eq_iff)
-  apply(simp add: inj_on_def)
-  done
-
-lemma atom_eqvt_raw:
-  fixes p::"perm"
-  shows "(p \<bullet> atom) = atom"
-  apply(perm_simp)
-  apply(simp)
-  done
-
-lemma supp_finite_at_set:
-  fixes S::"('a :: at) set"
-  assumes a: "finite S"
-  shows "supp S = atom ` S"
-  apply(rule finite_supp_unique)
-  apply(simp add: supports_def)
-  apply (rule finite_induct[OF a])
-  apply (simp add: eqvts)
-  apply (simp)
-  apply clarify
-  apply (subst atom_image_cong[symmetric])
-  apply (subst atom_eqvt_raw[symmetric])
-  apply (subst eqvts[symmetric])
-  apply (rule swap_set_not_in)
-  apply simp_all
-  apply(rule finite_imageI)
-  apply(rule a)
-  apply (subst atom_image_cong[symmetric])
-  apply (subst atom_eqvt_raw[symmetric])
-  apply (subst eqvts[symmetric])
-  apply (rule swap_set_in)
-  apply simp_all
-  done
-
-lemma supp_at_insert:
-  "finite (xs :: ('a :: at) set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs"
-  apply (simp add: supp_finite_at_set)
-  apply (simp add: supp_at_base)
-  done
-
 lemma supp_atom_finsert:
   "supp (finsert (x :: atom) S) = supp x \<union> supp S"
   apply (subst supp_fset_to_set[symmetric])
@@ -129,7 +80,8 @@
   done
 
 lemma supp_at_finsert:
-  "supp (finsert (x :: 'a :: at) S) = supp x \<union> supp S"
+  fixes S::"('a::at) fset"
+  shows "supp (finsert x S) = supp x \<union> supp S"
   apply (subst supp_fset_to_set[symmetric])
   apply (simp add: supp_finite_atom_set)
   apply (simp add: supp_at_insert[OF fin_fset_to_set])