diff -r 7a6b87adebc8 -r 66ef2a2c64fb Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Wed Apr 13 13:44:25 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Fri Apr 22 00:18:25 2011 +0800
@@ -2398,11 +2398,6 @@
 lemma list_renaming_perm:
   shows "\<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> (p \<bullet> set bs)"
 proof (induct bs)
-  case Nil
-  have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" 
-    by (simp add: supp_zero_perm)
-  then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
-next
   case (Cons a bs)
   then have " \<exists>q. (\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"  by simp
   then obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> p \<bullet> (set bs)"
@@ -2443,6 +2438,11 @@
   }
   ultimately show "\<exists>q. (\<forall>b \<in> set (a # bs). q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
     by blast
+next
+ case Nil
+  have "(\<forall>b \<in> set []. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> set [] \<union> p \<bullet> set []" 
+    by (simp add: supp_zero_perm)
+  then show "\<exists>q. (\<forall>b \<in> set []. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> set [] \<union> p \<bullet> (set [])" by blast
 qed