--- a/Nominal/Ex/Pi.thy	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/Ex/Pi.thy	Thu Apr 19 13:57:17 2018 +0100
@@ -380,7 +380,6 @@
   show  "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"
   and   "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"
   and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"
-    using assms
     apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)
     by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)
 qed