diff -r dce45db16063 -r c1af17982f98 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Wed Feb 03 10:50:24 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Wed Feb 03 11:21:34 2010 +0100
@@ -138,7 +138,7 @@
   apply(rule_tac x="pi \<bullet> pia" in exI)
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
-  apply(rule conjI)+
+  apply(rule conjI)
   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
   apply(simp add: a[symmetric] atom_eqvt eqvts)
   apply(rule conjI)