--- a/Nominal/Nominal2_Base.thy	Thu Jun 23 13:09:17 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu Jun 23 22:21:43 2011 +0100
@@ -2577,9 +2577,13 @@
   by (simp add: supp_atom [symmetric] supp_def atom_eqvt)
 
 lemma fresh_at_base: 
-  shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"
-  unfolding fresh_def by (simp add: supp_at_base)
-
+  shows  "sort_of a \<noteq> sort_of (atom b) \<Longrightarrow> a \<sharp> b"
+  and "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"
+  unfolding fresh_def 
+  apply(simp_all add: supp_at_base)
+  apply(metis)
+  done
+  
 lemma fresh_atom_at_base: 
   fixes b::"'a::at_base"
   shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"
@@ -2684,7 +2688,6 @@
 where
   "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
 
-
 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
   unfolding flip_def by (rule swap_self)
 
@@ -2841,13 +2844,22 @@
     unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
 qed
 
+lemma at_class_sort:
+  fixes s :: atom_sort
+  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+  fixes a::"'a"
+  assumes type: "type_definition Rep Abs {a. sort_of a = s}"
+  assumes atom_def: "\<And>a. atom a = Rep a"
+  shows "sort_of (atom a) = s"
+  using atom_def type
+  unfolding type_definition_def by simp
+
+
 setup {* Sign.add_const_constraint
   (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}
 setup {* Sign.add_const_constraint
   (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
 
-
-
 section {* The freshness lemma according to Andy Pitts *}
 
 lemma freshness_lemma: