--- a/Nominal/Nominal2_Base.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -2099,7 +2099,7 @@
 
 subsection {* Type @{typ "'a multiset"} is finitely supported *}
 
-lemma set_of_eqvt[eqvt]:
+lemma set_of_eqvt [eqvt]:
   shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"
 by (induct M) (simp_all add: insert_eqvt empty_eqvt)
 
@@ -2886,7 +2886,7 @@
   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
   assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
 
-declare atom_eqvt[eqvt]
+declare atom_eqvt [eqvt]
 
 class at = at_base +
   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"