diff -r b33b42211bbf -r 188826f1ccdb Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Thu Mar 13 09:30:26 2014 +0000
+++ b/Nominal/Ex/Pi.thy	Mon Mar 24 15:31:17 2014 +0000
@@ -172,8 +172,6 @@
   apply(auto simp add: fresh_star_def)[1]
   apply(blast)
   apply(simp)
-  apply(blast)
-  apply(simp)
   apply(case_tac b)
   apply(simp)
   apply(case_tac a)
@@ -192,9 +190,7 @@
   apply(blast)
   using [[simproc del: alpha_lst]]
   apply(auto simp add: fresh_star_def)[1]
-  apply(blast)
   apply(simp)
-  apply(blast)
   --"compatibility"
   apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])
   apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")