--- a/Nominal/Atoms.thy	Thu Jun 23 13:09:17 2011 +0100
+++ b/Nominal/Atoms.thy	Thu Jun 23 22:21:43 2011 +0100
@@ -65,7 +65,7 @@
 
 lemma sort_of_atom_name: 
   shows "sort_of (atom (a::name)) = Sort ''name'' []"
-  unfolding atom_name_def using Rep_name by simp
+  by (simp add: atom_name_def Rep_name[simplified])
 
 text {* Custom syntax for concrete atoms of type at *}
 
@@ -104,11 +104,10 @@
 
 atom_decl name2
 
-lemma sort_of_atom_name2:
-  "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []"
-unfolding atom_name2_def 
-using Rep_name2 
-by simp
+lemma 
+  "sort_of (atom (a::name2)) \<noteq> sort_of (atom (b::name))"
+by (simp add: sort_of_atom_name)
+
 
 text {* example swappings *}
 lemma