diff -r 2845e736dc1a -r 6911934c98c7 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Wed Feb 03 12:06:10 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Wed Feb 03 12:13:22 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)