diff -r 8639077e0f43 -r 7c607df46a0a Nominal/Nominal2_Supp.thy
--- a/Nominal/Nominal2_Supp.thy	Thu Mar 18 10:15:57 2010 +0100
+++ b/Nominal/Nominal2_Supp.thy	Thu Mar 18 11:33:37 2010 +0100
@@ -17,23 +17,23 @@
 definition 
   fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)
 where 
-  "xs \<sharp>* c \<equiv> \<forall>x \<in> xs. x \<sharp> c"
+  "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"
 
 lemma fresh_star_prod:
-  fixes xs::"atom set"
-  shows "xs \<sharp>* (a, b) = (xs \<sharp>* a \<and> xs \<sharp>* b)"
+  fixes as::"atom set"
+  shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)"
   by (auto simp add: fresh_star_def fresh_Pair)
 
 lemma fresh_star_union:
-  shows "(xs \<union> ys) \<sharp>* c = (xs \<sharp>* c \<and> ys \<sharp>* c)"
+  shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
   by (auto simp add: fresh_star_def)
 
 lemma fresh_star_insert:
-  shows "(insert x ys) \<sharp>* c = (x \<sharp> c \<and> ys \<sharp>* c)"
+  shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"
   by (auto simp add: fresh_star_def)
 
 lemma fresh_star_Un_elim:
-  "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
+  "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"
   unfolding fresh_star_def
   apply(rule)
   apply(erule meta_mp)
@@ -41,12 +41,12 @@
   done
 
 lemma fresh_star_insert_elim:
-  "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
+  "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"
   unfolding fresh_star_def
   by rule (simp_all add: fresh_star_def)
 
 lemma fresh_star_empty_elim:
-  "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
+  "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"
   by (simp add: fresh_star_def)
 
 lemma fresh_star_unit_elim: