--- a/Nominal/Nominal2_Base.thy	Wed Jan 19 19:06:52 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Jan 19 19:41:50 2011 +0100
@@ -2228,6 +2228,17 @@
   thus ?thesis ..
 qed
 
+lemma obtain_fresh':
+  assumes fin: "finite (supp x)"
+  obtains a::"'a::at_base" where "atom a \<sharp> x"
+using obtain_at_base[where X="supp x"]
+by (auto simp add: fresh_def fin)
+
+lemma obtain_fresh:
+  fixes x::"'b::fs"
+  obtains a::"'a::at_base" where "atom a \<sharp> x"
+  by (rule obtain_fresh') (auto simp add: finite_supp)
+
 lemma supp_finite_set_at_base:
   assumes a: "finite S"
   shows "supp S = atom ` S"
@@ -2539,10 +2550,7 @@
   assumes P: "finite (supp P)"
   shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
 proof -
-  obtain a::'a where "atom a \<notin> supp P"
-    using P by (rule obtain_at_base)
-  hence "atom a \<sharp> P"
-    by (simp add: fresh_def)
+  obtain a::'a where "atom a \<sharp> P" using P by (rule obtain_fresh')
   show "(FRESH x. f (P x)) = f (FRESH x. P x)"
     apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
     apply (cut_tac `atom a \<sharp> P`)
@@ -2562,11 +2570,9 @@
   and     Q: "finite (supp Q)"
   shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"
 proof -
-  from assms have "finite (supp P \<union> supp Q)" by simp
-  then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"
-    by (rule obtain_at_base)
-  hence "atom a \<sharp> P" and "atom a \<sharp> Q"
-    by (simp_all add: fresh_def)
+  from assms have "finite (supp (P, Q))" by (simp add: supp_Pair)
+  then obtain a::'a where "atom a \<sharp> (P, Q)" by (rule obtain_fresh') 
+  then have "atom a \<sharp> P" and "atom a \<sharp> Q" by (simp_all add: fresh_Pair)
   show ?thesis
     apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
     apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)