--- a/Nominal/Nominal2_Base.thy	Mon Jun 27 12:15:21 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon Jun 27 19:13:55 2011 +0100
@@ -2273,7 +2273,6 @@
   qed
 qed
 
-
 lemma supp_perm_perm_eq:
   assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"
   shows "p \<bullet> x = q \<bullet> x"
@@ -2291,18 +2290,17 @@
 text {* disagreement set *}
 
 definition
-  ds :: "perm \<Rightarrow> perm \<Rightarrow> atom set"
+  dset :: "perm \<Rightarrow> perm \<Rightarrow> atom set"
 where
-  "ds p q = {a::atom. p \<bullet> a \<noteq> q \<bullet> a}"
+  "dset p q = {a::atom. p \<bullet> a \<noteq> q \<bullet> a}"
 
 lemma ds_fresh:
-  assumes "ds p q \<sharp>* x"
+  assumes "dset p q \<sharp>* x"
   shows "p \<bullet> x = q \<bullet> x"
 using assms
-unfolding ds_def fresh_star_def fresh_def
+unfolding dset_def fresh_star_def fresh_def
 by (auto intro: supp_perm_perm_eq)
 
-    
 lemma atom_set_perm_eq:
   assumes a: "as \<sharp>* p"
   shows "p \<bullet> as = as"