diff -r 5af3a3203a76 -r 1fce03e3e8ad src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 12 16:21:07 2011 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Wed Oct 12 20:16:48 2011 +0200
@@ -653,7 +653,7 @@
   shows "\<exists>pi::name prm. p = pi \<bullet> q \<and> t = pi \<bullet> u \<and>
     set pi \<subseteq> (supp p \<union> supp q) \<times> (supp p \<union> supp q)"
   using assms
-proof (induct p arbitrary: q t u \<Delta>)
+proof (induct p arbitrary: q t u)
   case (PVar x T)
   note PVar' = this
   show ?case