--- a/Nominal/Nominal2_Base.thy	Mon Jun 27 08:42:02 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Mon Jun 27 12:15:21 2011 +0100
@@ -2287,6 +2287,21 @@
   then show "p \<bullet> x = q \<bullet> x"
     by (metis permute_minus_cancel permute_plus)
 qed
+
+text {* disagreement set *}
+
+definition
+  ds :: "perm \<Rightarrow> perm \<Rightarrow> atom set"
+where
+  "ds p q = {a::atom. p \<bullet> a \<noteq> q \<bullet> a}"
+
+lemma ds_fresh:
+  assumes "ds p q \<sharp>* x"
+  shows "p \<bullet> x = q \<bullet> x"
+using assms
+unfolding ds_def fresh_star_def fresh_def
+by (auto intro: supp_perm_perm_eq)
+
     
 lemma atom_set_perm_eq:
   assumes a: "as \<sharp>* p"