diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/Pi.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -179,6 +179,7 @@
 | "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"
 | "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
+  using [[simproc del: alpha_lst]]
   apply(auto simp add: piMix_distinct piMix_eq_iff)
   apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")
   unfolding eqvt_def
@@ -294,10 +295,12 @@
   apply(case_tac ba)
   apply(simp)
   apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))
+  using [[simproc del: alpha_lst]]
   apply(auto simp add: fresh_star_def)[1]
   apply(blast)
   apply(blast)
   apply(blast)
+  using [[simproc del: alpha_lst]]
   apply(auto simp add: fresh_star_def)[1]
   apply(blast)
   apply(simp)