--- a/Nominal/Nominal2_Base.thy	Fri Jun 24 09:42:44 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Sat Jun 25 21:28:24 2011 +0100
@@ -2571,6 +2571,11 @@
 class at = at_base +
   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
 
+lemma sort_ineq [simp]:
+  assumes "sort_of (atom a) \<noteq> sort_of (atom b)"
+  shows "atom a \<noteq> atom b"
+using assms by metis
+
 lemma supp_at_base: 
   fixes a::"'a::at_base"
   shows "supp a = {atom a}"