--- a/Nominal/Atoms.thy	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/Atoms.thy	Tue May 10 07:47:06 2011 +0100
@@ -225,10 +225,12 @@
 
 declare [[coercion "atom::var2\<Rightarrow>atom"]]
 
+(*
 lemma
   fixes a::"var1" and b::"var2"
   shows "a \<sharp> t \<and> b \<sharp> t"
 oops
+*)
 
 (* does not yet work: it needs image as
    coercion map *)