--- a/Quot/Nominal/Terms.thy	Thu Feb 18 08:43:13 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 18 09:46:38 2010 +0100
@@ -1076,14 +1076,11 @@
 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
 print_theorems
 
-abbreviation
-  "atoms xs \<equiv> {atom x| x. x \<in> xs}"
-
 local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *}
 print_theorems 
 
 (*
-doesn't work yet
+Doesnot work yet since we do not refer to fv_ty
 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}
 print_theorems
 *)
@@ -1091,12 +1088,12 @@
 primrec
   fv_tyS
 where 
-  "fv_tyS (All xs T) = (fv_ty T - atoms xs)"
+  "fv_tyS (All xs T) = (fv_ty T - atom ` xs)"
 
 inductive
   alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
 where
-  a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) fv_ty pi (atoms xs2, T2)) 
+  a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2)) 
         \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
 
 lemma