--- a/Nominal/Test.thy	Thu Mar 04 10:59:52 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 04 11:16:36 2010 +0100
@@ -71,20 +71,22 @@
 apply (simp_all add: weird_inj)
 apply (erule conjE)+
 apply (erule exE)+
+apply (erule conjE)+
+apply (erule exE)+
 apply (rule conjI)
 apply (rule_tac x="pica + pic" in exI)
 apply (erule alpha_gen_compose_trans)
 apply assumption
 apply (simp add: alpha_eqvt)
+apply (rule_tac x="pia + pib" in exI)
+apply (rule_tac x="piaa + piba" in exI)
+apply (rule conjI)
+apply (erule alpha_gen_compose_trans)
+apply assumption
+apply (simp add: alpha_eqvt)
 apply (rule conjI)
 defer
-apply (rule_tac x="pia + pi" in exI)
-apply (erule alpha_gen_compose_trans)
-apply assumption
-apply (simp add: alpha_eqvt)
-(* Normally: (pia + pb + (pib + pa)) *)
-apply (rule_tac x="piaa + pib" in exI)
-apply (rule_tac x="piab + piba" in exI)
+apply (rule_tac x="pid + pi" in exI)
 apply (erule alpha_gen_compose_trans)
 apply assumption
 apply (simp add: alpha_eqvt)