--- a/Nominal/Atoms.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Atoms.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -210,7 +210,7 @@
   shows "ty_of (p \<bullet> x) = ty_of x"
   unfolding ty_of_def
   unfolding atom_eqvt [symmetric]
-  by simp
+  by (simp only: sort_of_permute)
 
 
 section {* Tests with subtyping and automatic coercions *}
@@ -236,6 +236,7 @@
 lemma
   fixes as::"var1 set"
   shows "atom ` as \<sharp>* t"
+
 oops
 
 end