--- a/Nominal/Ex/TypeVarsTest.thy	Wed Feb 16 14:44:33 2011 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Thu Feb 24 16:26:11 2011 +0000
@@ -38,6 +38,12 @@
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
 
+(* FIXME: only works for type variables 'a 'b 'c *)
+
+nominal_datatype ('a, 'b, 'c) psi =
+  PsiNil
+| Output "'a" "'a" "('a, 'b, 'c) psi" 
+
 
 end
 

--- a/Nominal/Nominal2_Abs.thy	Wed Feb 16 14:44:33 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy	Thu Feb 24 16:26:11 2011 +0000
@@ -768,6 +768,15 @@
   unfolding fresh_star_def
   by(auto simp add: Abs_fresh_iff)
 
+lemma Abs_fresh_star2:
+  fixes x::"'a::fs"
+  shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_set bs x \<longleftrightarrow> as \<sharp>* x"
+  and   "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_res bs x \<longleftrightarrow> as \<sharp>* x"
+  and   "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* Abs_lst ds x \<longleftrightarrow> cs \<sharp>* x"
+  unfolding fresh_star_def Abs_fresh_iff
+  by auto
+
+
 lemma Abs1_eq:
   fixes x::"'a::fs"
   shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"

--- a/Nominal/Nominal2_Base.thy	Wed Feb 16 14:44:33 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Feb 24 16:26:11 2011 +0000
@@ -1654,7 +1654,6 @@
 done
 
 lemma fresh_star_atom_set_conv:
-  fixes p::"perm"
   assumes fresh: "as \<sharp>* bs"
   and     fin: "finite as" "finite bs"
   shows "bs \<sharp>* as"
@@ -1662,6 +1661,13 @@
 unfolding fresh_star_def fresh_def
 by (auto simp add: supp_finite_atom_set fin)
 
+lemma atom_fresh_star_disjoint:
+  assumes fin: "finite bs" 
+  shows "as \<sharp>* bs \<longleftrightarrow> (as \<inter> bs = {})"
+
+unfolding fresh_star_def fresh_def
+by (auto simp add: supp_finite_atom_set fin)
+
 
 lemma fresh_star_Pair:
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
@@ -1747,14 +1753,6 @@
 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
 done
 
-lemma at_fresh_star_inter:
-  assumes a: "(p \<bullet> bs) \<sharp>* bs" 
-  and     b: "finite bs"
-  shows "p \<bullet> bs \<inter> bs = {}"
-using a b
-unfolding fresh_star_def
-unfolding fresh_def
-by (auto simp add: supp_finite_atom_set)
 
 
 section {* Induction principle for permutations *}